text:
Buteshire (UK Parliament constituency)

Buteshire was a county constituency of the House of Commons of the Parliament of Great Britain from 1708 to 1801 and of the Parliament of the United Kingdom from 1801 to 1918.

Creation
The British parliamentary constituency was created in 1708 following the Acts of Union, 1707 and replaced the former Parliament of Scotland shire constituency of Buteshire.

History
From 1708 to 1832 Buteshire and Caithness were paired as alternating constituencies: one of the constituencies elected a Member of Parliament (MP) to one parliament, the other to the next. The areas which were covered by the two constituencies are quite remote from each other, Caithness in the northeast of Scotland and Buteshire in the southwest.

From 1832 to 1918, Buteshire was represented continuously by its own MP.

Boundaries
From 1708 to 1832, the Buteshire constituency covered the county of Bute (which historically included the islands of Arran, Great Cumbrae and Little Cumbrae) minus the parliamentary burgh of Rothesay, which was a component of the Ayr Burghs constituency. In 1832, Rothesay was merged into the Buteshire constituency.

By 1892, Bute had become a local government county and, throughout Scotland, under the Local Government (Scotland) Act 1889, county boundaries had been redefined for all purposes except parliamentary representation. 26 years were to elapse before constituency boundaries were redrawn, by the Representation of the People Act 1918, to take account of new local government boundaries.

In 1918, the Bute and Northern Ayrshire county constituency was created, to cover the county of Bute and a northern portion of the county of Ayr. The rest of the county of Ayr was divided between three other constituencies, all entirely within the county: the county constituencies of South Ayrshire and Kilmarnock, and a remodelled Ayr Burghs.

Elections in the 1830s

 * Gain from Non Partisan at, which returned the 1826 MP as this seat's alternating pair

For the 1831 election, Caithness returned the MP.

 * Considered a 'new seat' as the constituency did not elect an MP in 1831

Stuart resigned, causing a by-election.

Elections in the 1840s
Rae was appointed Lord Advocate, requiring a by-election.

Rae's death caused a by-election.

Stuart-Wortley was appointed Judge Advocate General of the Armed Forces, requiring a by-election.

Elections in the 1850s
Stuart-Wortley was appointed Solicitor General for England and Wales, requiring a by-election.

Elections in the 1860s
Mure's appointment as a Senator of the College of Justice, becoming Lord Mure, caused a by-election.

Elections in the 1880s
Russell was disqualified due to his holding of a government contract at the time of the election, causing a by-election.

Dalrymple was appointed a Lord Commissioner of the Treasury, requiring a by-election.

Robertson was appointed as Solicitor General for Scotland, requiring a by-election.

license: Creative Commons - Attribution Share-Alike - https://creativecommons.org/licenses/by-sa/4.0/

title: Buteshire (UK Parliament constituency)


text:
Talk:Safa and Marwa

We're not going to get lengthy articles on each of Safa and Marwah; also, given the fact that they are almost exclusively referred to together, this should be sufficient justification for the name change. ---Mpatel (talk) 17:00, August 26, 2005 (UTC)

Distances
The distances shown appear to be incorrect. Safa is closer to the Kaaba than Marwah. I don't want to do original research by measuring them out on a map — maybe someone can find better distance references. --Cam 12:57, 13 January 2006 (UTC)

 * Safa is closer to Aswad corner as compared to Mawa from Iraqi corner of Kaaba. Distances shown are not wrong. These can be measured from Google earth. Afzal212 (talk) 12:25, 25 March 2024 (UTC)

Alternative view I deleted the details regarding the alternative view. A brief mention is sufficient, and moreover the exposition of the alternative view was less than clear. It conflated the Arabic roots s-f-w and s-f-f and misrepresented Qur'an 2:158, among other problems. —Preceding unsigned comment added by 99.141.167.56 (talk) 05:54, 12 May 2009 (UTC)

As-Safa and Al-Marwah
The Term "Al Safa" is not proper Arabic, is it? See: Sun and moon letters. 62.65.135.34 (talk) 10:42, 7 November 2011 (UTC)

 * اِنَّ الصَّفَا وَ الۡمَرۡوَۃَ مِنۡ شَعَآئِرِ اللّٰہِ
 * Quran 2:158 Afzal212 (talk) 00:20, 24 March 2024 (UTC)

Sa'i does not mean ritual walking.
Sa'i does not mean ritual walking. Sa'i means "seeking" or "search", one seeks the guidance of God. Hajar went back and forth seeking water, as well as seeking the aid of God. The modern statment "'Es'a ela rabik" loosely meaning, "turn to God and seek his help." 8227 16:04, 16 November 2015 (UTC) — Preceding unsigned comment added by A8227 (talk • contribs)

This article should be classified as incomplete/stub
This article should be classified as a stub as it is lacking comprehensive historical data, rather it just takes a islamic theological perspective. The Ahadith describe pre-islamic practices carried out by polytheists at these sites and an honest discussion about those and an inclusion of a subsection would only do the amazing history of those places justice. Avoiding a balanced discussion on these matters renders this article unidimensional and misleading. Wikipedia owes its readers the most comprehensive and informative description of the matters at hand.

Safa and Marwa shown on wrong side of Kaaba
The poison of safa صفا starts on Aswad side and walk Saee سعی to Marwa مروہ goes northwards Please consider correction as per actual Afzal212 (talk) 07:09, 12 June 2023 (UTC)

If I have correctly understood your comment, it refers to the black-and-white drawing at the start. If I am wrong, stop reading. I feel that it is a drawing showing what is seen from Abu Queis (thus with the north in the bottom-right corner), not a map that must have the north at top. I am the author of the next comment (a curious, not an expert). 151.29.137.229 (talk) 18:36, 1 July 2023 (UTC)

 * Sir Regards Afzal212 (talk) 15:02, 2 July 2023 (UTC)
 * Though it is for information of masses kindly let me submit for reconsiding
 * "Irrespective of north south the massah Safa to Marwa is on Door side of Kaaba i.e Hajr.e.Aswad corner to Iraqi corner" Afzal212 (talk) 04:26, 4 July 2023 (UTC)

7*450=3150
Thus 3600 is incorrect, unless something considered implicit is not stated. 151.29.137.229 (talk) 07:38, 1 July 2023 (UTC) Moreover, the distance cannot exceed 130+300=430 m, that is realized if the hills are NE-SW (or like) of the Kaaba. 8If are one SE and one NE (as said in the text), the distance should be around sqr(130^2+300^2)~330 m. — Preceding unsigned comment added by 151.29.137.229 (talk) 10:04, 1 July 2023 (UTC) I have found a map of the Mosque showing that are actually one SE and one NE. Comparing with an atlas of the region, they seem151.29.137.229 (talk) 10:41, 1 July 2023 (UTC) BOTH satellites of Abu Qubeis

 * Safa to Marwa peak of domes over two hills are 390 meter as per measurement at google earth Afzal212 (talk) 00:17, 24 March 2024 (UTC)

Door of kaaba shown on wrong side
Though it is sketch for knowledge of layman yet confusing due to direction of door of kaaba with respect to safa. Actually Aswad corner near door is the point nearest to Safaa. Having visited the grand mosque three for Umrah twice and Hajj once. The position of wall containing door of kaaba is on east side facing the line from Safa to Mrwa with tilt about 30 degree angle. It is seen on Google earth. I intended to submit corrected sketch but there was no option to submit Pic. Please consider correction as per actual on ground. Afzal212 (talk) 08:59, 16 March 2024 (UTC)

 * Thanks for talk option but if the wrong misguiding sketch can not be corrected before day of judgment, no use to waste time in suggesting edit to rectify apparent big mistake. Afzal212 (talk) 16:12, 28 June 2024 (UTC)

title: Talk:Safa and Marwa


text:
Talk:Bible Stories

(requested)
Did someone try to delete this page? It was on the requested articles page, so I thought I would start it. — Preceding unsigned comment added by 67.80.139.189 (talk • contribs) 17:00, 26 August 2005 (UTC)

More Work Needed
This page isn't a bad idea, but more work should be done on it if someone has some time. For some of these stories, the entire story could be told on this page. For those stories that are of a certain length, a summary could appear here with a link to another article that might already exist, or which could be newly written. Or at the very least, I suggest that each story contain a bible reference, linking to the Wikisource Bible like this: John 20. Readparse 14:39, 13 October 2005 (UTC)

"Move" and copy this talk
This is a WP:redirect to Bible while "Bible stories" (lowercase) redirects to the stub Bible story. I will change this target to "Bible story", link this talk and old redirect content there. ... ✅ See Bible story. --P64 (talk) 19:53, 20 July 2012 (UTC)

title: Talk:Bible Stories


text:
Garden District, Toronto

The Garden District is a neighbourhood in downtown Toronto, Ontario, Canada. The name was selected by the Toronto East Downtown Residents Association (TEDRA) in recognition of Allan Gardens, an indoor botanical garden located nearby at the intersection of Carlton and Jarvis Streets. The Garden District was officially designated by the Mayor and Toronto City Council in 2001, while TEDRA has since been renamed the Garden District Residents Association. Part of the neighbourhood is within official City of Toronto neighbourhood of Moss Park.

As defined by the Association, the neighbourhood is bordered by Carlton Street to the north, Yonge Street to the west, Sherbourne Street to the east and Queen Street to the south. This area includes the southern part of Toronto’s Gay Village and heritage sites such as the Mackenzie House Museum, Gallery Arcturus and the Merchandise Building.

Character
This neighbourhood consists of two distinct areas: The western portion, from Yonge Street to Jarvis Street, was first subdivided at the time Toronto was incorporated as a city in 1834 from the McGill Estate (the owner John McGill died that year). This area quickly filled with overflow from central Toronto and includes a number of early, mostly non-government (especially religious) institutions such as the Metropolitan Methodist Church (Metropolitan United Church after church union in the 1920s), St Michael's Roman Catholic Cathedral, the Roman Catholic Bishop's Palace, St. Michael's Choir School and St Michael's Hospital, places of entertainment such as Massey Hall, the Elgin and Winter Garden Theatres, the Canon Theatre (formerly Pantages Theatre) and Maple Leaf Gardens as well as the Ryerson Model School (now a part of Toronto Metropolitan University (TMU)) TMU's campus today stretches from Gerrard in the north, east to Mutual and south of Gould, west to Yonge, and includes The Image Centre, a photographic museum which is home to The Black Star Collection and the yearly Scotiabank Contact Photography Festival. The eastern portion from Jarvis Street to Sherbourne was largely subdivided later in the 1850s from the Jarvis Estate (Hazelburn) and the Allan Estate (Moss Park) with north-south streets based on the street grid of the original Town of York. This area is largely residential with two parks (Moss Park and Allan Gardens) and a large number of local churches. It was originally a very exclusive district and declined in time as the housing stock aged and smaller lots for workers were built. This area has seen a large replacement of older homes with residential, institutional and commercial development. Located in the eastern portion of the Garden District, Walnut Hall were four Georgian styled terraced homes. On May 18, 2007, local uproar arose over its demolition. Constructed in 1856 and designated as a heritage site in 1997, the building was nonetheless neglected and began to collapse.

The Garden District includes a mix of housing, from million-dollar condos, renovated Victorian villas, and Edwardian row houses to apartment co-operatives, subsidized housing units, and many hostels and shelters. George Street, one block east of Jarvis has a blighted area around the Seaton House shelter. The City of Toronto government is planning to redevelop the site incorporating heritage homes now boarded up.

Demographics
There is a substantial Francophone presence because of the area’s French-language institutions near the neighbourhood, including Paroisse Sacré Cœur, a Roman Catholic parish, Le Collège français, and École élémentaire Gabrielle-Roy. Le Collège français and École élémentaire Gabrielle-Roy are both operated by Conseil scolaire Viamonde, a secular public school board.

A separate neighbourhood association, the McGill-Granby Village Resident's Association, represents the residents of the area around those two streets.

There are several institutions related to the Aboriginal community along Gerrard Street, the south of Allan Gardens. They include Miziwe Biik Aboriginal Employment and Training, Anishnawbe Health Toronto, and Native Women's Resource Centre of Toronto. According to 2011 National Household Survey, the population with Aboriginal Ancestry of census tract 5350032.00 grew from 105 in 2005 to 165 in 2010. This large increase (+57%) is significant when the total population of CT5350032.00 decreased by almost 4%.

Transportation
The area is well served by public transit, with the 505 Dundas, 506 Carlton east-west streetcar routes. The 75 Sherbourne bus runs north-south along Sherbourne. The Yonge-University-Spadina subway Line 1 runs north-south along Yonge Street to the west.

title: Garden District, Toronto


text:
User talk:Ipnumber

Welcome
Welcome!

Hello,, and welcome to Wikipedia! Thank you for your contributions. I hope you like the place and decide to stay. Here are a few good links for newcomers: I hope you enjoy editing here and being a Wikipedian! Please sign your name on talk pages using four tildes (~~); this will automatically produce your name and the date. If you need help, check out Where to ask a question, ask me on my talk page, or place  on your talk page and someone will show up shortly to answer your questions. Again, welcome! Friday (talk) 17:01, 26 August 2005 (UTC)
 * The five pillars of Wikipedia
 * How to edit a page
 * Help pages
 * Tutorial
 * How to write a great article
 * Manual of Style

Hungry Man
I linked Hungry Man to TV dinner. In fact, given the nice amount of information in TV dinner, I'm half tempted to make Hungry man a redirect to that. What do you think? Friday (talk) 17:03, 26 August 2005 (UTC)

Short articles
Hey, I noticed a couple of your new articles, like The Star gazer and Listen to your heart. These are so short that it'll be hard for us to know what to do with them. Generally, we like new articles to be created only when there's enough information for someone who's never heard of the topic before. Could you take a few minutes and fill them so we know more about them and why they're important? Thanks! Friday (talk) 20:08, 27 August 2005 (UTC)
 * Nevermind, they're not there anymore. Friday (talk) 20:54, 27 August 2005 (UTC)

Reference desk
Could you expand your questions on the Reference desk? It's difficult to answer incomplete questions. — Laura Scudder | Talk 20:28, 27 August 2005 (UTC)

title: User talk:Ipnumber


text:
Isaac Sears

Isaac Sears (1 July 1730 – 28 October 1786) was an American merchant, sailor, Freemason, and political figure who played an important role in the American Revolution.

He was born July 1, 1730, at West Brewster, Massachusetts, the son of Joshua and Mary Sears. He was a descendant of Richard Sears, who emigrated to the colonies from Colchester, England, in 1630. While he was a child, the family moved to Norwalk, Connecticut.

At the age of sixteen, he was apprenticed to the skipper of a coastal vessel. By 1752, he was in command of a sloop trading between New York and Canada. Sears established his reputation as a privateer during the French and Indian War, commanding a vessel from 1758 until 1761, when he lost his ship. He moved to New York City and had become successful enough to become a merchant investing in ships engaging in trade with the West Indies.

Early life
Born in July 1730 in West Brewster, Barnstable Massachusetts Bay Colony, the son of Joshua and Mary (Thacher) Sears. Isaac Sears was the sixth of nine children. He was a fifth generation of New Englander whose family left Cape Cod and settled in Norwalk, Connecticut. He had well established Religious ties, as he also had ancestors who were a Deacon and a Minister in the Congregational Church. He was baptized in the church in 1730, moreover, he would go on to be a member of the Congregation in Harwich Mass. He would later go on to become an Anglican and marry Sarah Drake at Trinity Church in New York, and raised his family in Manhattan. His Father-in-law was Jasper Drake who owned the Water Street Tavern.

As a young boy he sold shellfish, and by sixteen had begun apprenticing to the Captain of a New England coastal vessel. After ample time learning the trade, he was commissioned as an officer. By his twenties he commanded small sloops that sailed the North American coast between Halifax and New York. Some of these sloops would see him travel as far as the West Indies, even during the winter. By 1752, he was in command of a sloop trading between New York and Canada. During the Seven Years' War he became a Captain of privateers and commanded The Decoy a six gun sloop, The Catherine, and The Belle Isle which had fourteen guns. Sears established a reputation during the French and Indian War and became Captain of several privateers. He was commissioned to prey on enemy ships from 1758 until 1761, when he ultimately lost his ship. He moved to New York City and had become successful enough to become a merchant investing in ships engaging in trade with the West Indies. By 1763 he underwent a career change in which he moved on from captaining ships, to settle as a merchant. He started first in vessels but The Sugar Act of 1764 affected his trade along the North American coast, and West Indies and ultimately forced him to stop trade with Madeira.

Sons of Liberty
Sears and his fellow Sons of Liberty all gathered at a coffee house on October 31, 1765, the day before the Stamp Act was to take effect. They ultimately resolved to enforce the opposition to the distribution of the stamps and formed an association to stop the importation of British goods until the act was rescinded. Sears organized and was a known leader of the Sons of Liberty in 1765. They used violence and threats of violence to prevent the use of stamps, moreover, Sears issued a death threat to anyone breaking the non-importation agreement before the colonies agreed to do so. He was nicknamed "King Sears" by aristocrats who feared his power to mobilize people in the streets and for his influential role in organizing and leading the New York mob. He was a most militant and influential agitator and earned a reputation for bravery and sought to limit the scope of Britain's authority in 1760. Another nickname that was bestowed upon him by British military engineer and cartographer John Montresor·, was the “Spawn of Liberty and Inquisition” which Montresor both passionately and derisively called him and his posse of vigilantes. British Vice Admiral Samuel Graves lists Sears as the “most active leaders and agitators of the rebellion.

He was at the head of nearly every demonstration of mob violence in New York City. He partnered with James DeLancey in opposition to the stamps and supported him in his 1768 election to the New York assembly. Sears and many of his followers were engaged in trade and demanded that trade continue without stamps.

In 1766, Sears, John Lamb and three others formed a committee of correspondence to communicate with other Sons of Liberty groups in other provinces. After the Stamp Act was repealed the Sons of Liberty erected a Liberty pole to celebrate. The liberty pole was a galling sight to the redcoats and a symbol of pride and defiance to the townsfolk. When the British cut down the pole for the first time, Sears and Walter Quackenbos collared  two redcoats posting broadsides, a fellow soldier drew his bayonet and threatened them, Sears had a rams horn in his hand and threw it at him and hit him in the head. In 1768, he and numerous New York merchants sent a petition to Parliament outlining their grievances on the state of trade. In 1769, when the New York assembly passed an appropriation for funding of the Quartering Act, he posted an inflammatory broadside entitled "To the betrayed inhabitants of the city and colony of New York".

On January 19, 1770, the Battle of Golden Hill began when Sears took it upon himself to prevent a half dozen redcoats from posting broadsides at an outdoor market near the East River wharves, Sears seized the soldier fixing the paper by the collar and asked him what business he had to put up Libels against the inhabitants and carried him to the mayor. The fifth liberty pole was raised on February 6, 1770 on a plot of land owned by Sears. When the Tea Act was passed in 1773, he organized the city's captains into refusing to freight the East Indian tea. It was the first organized opposition to the tax. Broadsides, signed "The Mohawks", were posted warning against anyone trying to land tea. New York's opposition was partly responsible for Boston's decision to stop the landing of tea. Adams wrote, "we must venture, and unless we do, we shall be discarded by the sons of liberty in the other colonies". They were successful in preventing the landing of tea. In April 1774, they boarded the Nancy and destroyed its tea.

During the Townsend Acts, Britain passed a Tea Act in 1773 to ship tea directly to North America to help the East India Company, saving it from being taxed so it can come out of bankruptcy. Sears and his companions believed that the ruin of their commerce was inevitable if they did not succeed in preventing the sale of India Company tea in America. They were convinced that this could only be effected by total prohibition of English tea, since the Company would find ways of importing its tea to America by way of private merchants regardless. He was also worried Britain would soon try to make a monopoly of other goods in the colonies, threatening the welfare of the Sons of Neptune. Before the tea was to be sent to the colonies, Captain Sears and McDougall decided an opposition was needed and sought to unite all the Sons of Neptune and Liberty with the merchants and tea-smugglers. The Sons of Liberty and the Dutch smugglers had come together and sparked the "New Flame" described by William Smith. As the tea approached the harbors of New York, Philadelphia, and Boston in early November the campaign began. The tea stood in the boats that were in the harbor and no one dared to remove them for fear of the tea being destroyed. Towards the end of November, McDougall from Sons of Liberty made a publication to be sent out to all harbors. "If any of the tea by any persons associated with the India Tea Company had accepted a commission to sell, land, or store the tea would be paid "an unwelcomed visit, in which they shall be treated as they deserve: by 'The Mohawks.'" Thus Sears and McDougall initiated the use of this distinctively American name to cover the identity of those who were ready to employ violence to block the operation of the Tea Act." Not long after, the Boston Tea Party took place and the tea ships in Philadelphia and New York turned back to England for fear of their cargo.

When in May 1774 news of the Boston Port Act arrived, Sears and McDougall wrote a letter of support to Boston, without consulting anyone else, in addition to a British boycott, they proposed a ban on exports to the West Indies and called for a Continental Congress. Reaction in New York to the Boston Port Act was cautious and equivocal, there was a split with the DeLanceys on whether to proceed with nonimportantion.

Committee of Sixty
On May 16, 1774, a meeting at the Fraunces Tavern was called of the various factions. The Committee of Fifty was elected with Isaac Low as its chairman. James DeLancey's faction was in the majority, with Sears and his Sons of Liberty in the minority.

In 1774, he was a leading member of New York City's Committee of Sixty. In a letter to the Boston Committee of Correspondence he proposed a meeting of delegates from the principal towns. This proposal was initially disavowed by the Committee of Sixty, but later was ratified in a proposal for the meeting of the First Continental Congress.

American Revolution
On April 15, 1775, he was arrested for his anti-British activities, but was rescued at the prison door by his supporters and paraded through the streets as a hero. When news of the Battle of Lexington arrived he and his followers seized the arsenal at the Custom House. He was the de facto commander of New York City until Washington's Army arrived in June, 1776.

On November 20, 1775, Sears led a group of 80 citizens in apprehending Parson Seabury, Judge Fowler, and Lord Underhill. At some point the mob forced Fowler to write (or else they forged his name) an apology and a promise not to interfere with the Second Continental Congress. While some of the mob escorted the three prisoners to Connecticut, ·November 23, 1775, Sears and his men rode into New York at high noon with bayonets fixed and shut down James Rivington's Gazetteer by taking all of the type from his office at the foot of Wall Street where a large crowd gathered outside the Merchants coffee shop to cheer the raiders as they marched out of town to the tune of Yankee Doodle. However, this action was condemned by the Committee of Sixty, the New York Provincial Congress and the New York delegation to the Continental Congress, but public opinion was with him and no action and after the capture of New York, Sears returned to Massachusetts, where he grew rich by privateering and spending time at sea as a privateer from Boston from 1777 to 1783. He formed partnerships with other privateers, such as John Kendrick, with whom he owned in partnership the vessel Count d'Estaing, commanded by Kendrick.

Post-war years
After the British left New York City in 1783, he returned to the city installing himself in a mansion on the Bowling Green and reviving the Sons of Liberty. By March, he was calling for the expulsion of any remaining Loyalists in the state by May 1. He and other members of the Sons of Liberty won enough seats in the New York State Assembly in December, 1784 to enact a set of harsh anti-Loyalist laws. He was exposed for buying up soldier's pay certificates at depressed prices and using them to speculate in forfeited Loyalist property. The public regarded this as the height of venality and cynicism. He was again elected to the assembly in 1786, but by then he was deeply in debt and he left the state to avoid arrest. Sears died in October 1786 of fever and dysentery contracted in Batavia in the Dutch East Indies while on a great adventure to open American trade with China, where he would be buried on an island in Canton Harbor.

title: Isaac Sears


text:
Talk:William Peters (lawyer)

Comment
Can someone more familar with american history please correct Whigs?

title: Talk:William Peters (lawyer)


text:
1965–66 NHL season

The 1965–66 NHL season was the 49th season of the National Hockey League. Six teams each played 70 games. The Montreal Canadiens won their second consecutive Stanley Cup as they defeated the Detroit Red Wings four games to two in the final series.

League business
A new trophy was introduced for this season. Jack Adams won the first Lester Patrick Trophy for his contribution to hockey in the United States.

February saw the momentous announcement that six conditional franchises had been awarded to Los Angeles, San Francisco, St. Louis, Minneapolis–St. Paul, Philadelphia and Pittsburgh, all to begin play in 1967. The St. Louis franchise was surprising, as no formal application from the city had been tendered. It was awarded to fulfill the wishes of James D. Norris and Arthur Wirtz, owners of the Chicago Black Hawks, who also owned the St. Louis Arena, which they wanted to sell.

On the debit side, a strong bid from Vancouver was rejected, much to the anger of many Canadians and the protest of their Prime Minister Lester Pearson. A rumour was widely spread — fuelled by a corroborating statement from Leafs' general manager Punch Imlach that the Toronto and Montreal owners had vetoed the bid out of a dislike for sharing the proceeds from television broadcasts of the games. Vancouver would eventually get an NHL franchise in 1970.

The Canadian Amateur Hockey Association (CAHA) called for the end the direct sponsorship of junior ice hockey team and to allow players who graduated from junior hockey to be chosen in the NHL Amateur Draft. CAHA president Lionel Fleury asked the NHL to terminate the existing professional-agreement rather than letting it expire in 1968. NHL president Clarence Campbell declined to terminate the agreement since 95 per cent of NHL players were produced by sponsored junior teams. The NHL felt that a draft of players might be viable but wanted to draft players at a younger age than 20, and wanted to continue making payments directly to amateur teams instead of the CAHA dispersing funds as it saw fit. Discussions remained unresolved until a new agreement with the requested changes was reached in August 1966.

Rule changes
The only significant rule change for this season was a requirement that the teams suit up two goaltenders for each game.

Regular season
Among notable players to debut during this season were Ed Giacomin for the Rangers, Bill Goldsworthy for the Bruins, Ken Hodge for Chicago and Mike Walton for Toronto. In the meantime, however, the career of future Hockey Hall of Famer Ted Lindsay was over, as his request for reinstatement as an active player was vetoed by the Toronto ownership.

Ed Giacomin put together a six-game unbeaten streak early in the season to the delight of the fans. But the Rangers' inexperience behind the blueline caught up with them as the team began to lose and the Rangers were out of contention quickly, which cost coach Red Sullivan his job. Emile Francis took over the coaching reins, but the Rangers were headed nowhere this season.Worse, Rod Gilbert had to undergo a second spinal fusion surgery if he wanted to play hockey again. The Rangers missed his offense.

Gordie Howe scored his 600th NHL goal in Montreal on November 27 in a 3–2 loss to the Canadiens to the cheers of the local fans. Among lesser milestones in the season were Frank Mahovlich's 250th goal and Johnny Bucyk's and Claude Provost's 200th.

In an unusual incident, the Red Wings' jerseys were stolen from the visitors' dressing room in Montreal the night before a January game, and Detroit was compelled to play in the uniforms of their junior farm team in Hamilton, which were express shipped to Montreal in time for the match.

James D. Norris, owner of the Chicago Black Hawks, died of a heart attack in late February.

Semifinals
The second game of the semifinal series between Detroit and Chicago on April 10, was nationally televised in the United States.

For the fourth straight year, it was Montreal vs. Toronto and Detroit vs. Chicago in the first round. The Canadiens were victorious over the Leafs in four straight games, while the Wings beat the Hawks in six.

(1) Montreal Canadiens vs. (3) Toronto Maple Leafs
The Montreal Canadiens were the best regular season team, earning 90 points. The Toronto Maple Leafs earned the third seed with 79 points. This was the twelfth playoff series between these two rivals, with Toronto winning six of their eleven previous series. This was a rematch from the 1965 semifinals, where Montreal won in six games. Toronto won sixteen of twenty-eight points in this year's regular season series.

The Canadiens defeated the Maple Leafs in a four-game sweep.

(2) Chicago Black Hawks vs. (4) Detroit Red Wings
The Chicago Black Hawks earned the second seed with 82 points. The Detroit Red Wings earned the fourth seed with 74 points. This was the eighth playoff series between these two rivals, with Detroit winning four of their seven previous series. This was a rematch of the 1965 semifinals, where Chicago won in seven games. Chicago earned twenty-four of twenty-eight points in this year's regular season series.

The Red Wings upset the Black Hawks in six games.

Stanley Cup Finals
The Montreal Canadiens were the defending champions in their twenty-second Stanley Cup Finals, after winning their thirteenth championship the previous year with a seven-game victory over the Chicago Black Hawks. This was the Detroit Red Wings' eighteenth Stanley Cup Finals, having won seven championships previously. Their most recent Finals came in 1964, when they lost to the Toronto Maple Leafs in seven games. This was the eleventh playoff series between these two teams, with Detroit winning seven of their ten previous series. Their most recent series had come in the 1958 semifinals, where Montreal won in a four-game sweep. Montreal won eighteen of twenty-eight points in this year's regular season series. Detroit would not return to the Stanley Cup Finals again until 1995.

Behind the skilled goaltending of Roger Crozier, who had missed parts of the regular season with illness, the Red Wings won the first two games of the Finals. However, Crozier was injured in the fourth game and the Canadiens won the Cup four games to two. Roger Crozier won the Conn Smythe Trophy as a member of the losing team.

Awards
Bobby Hull set a new record for goals in a season with 54 and a new record for points in a season with 97, earning him the Art Ross Trophy and his second straight Hart Trophy as the league's most valuable player. No left-winger would pace the NHL in points again until Alexander Ovechkin in 2007–08. Jacques Laperriere of Montreal won the Norris Trophy as best defenceman.

Scoring leaders
Note: GP = Games played, G = Goals, A = Assists, Pts = Points, PIM = Penalties in minutes Source: NHL.

Leading goaltenders
Note: GP = Games played; Min = Minutes played; GA = Goals against; GAA = Goals against average; W = Wins; L = Losses; T = Ties; SO = Shutouts

Coaches

 * Boston Bruins: Milt Schmidt
 * Chicago Black Hawks: Billy Reay
 * Detroit Red Wings: Sid Abel
 * Montreal Canadiens: Toe Blake
 * New York Rangers: Emile Francis
 * Toronto Maple Leafs: Punch Imlach

Debuts
The following is a list of players of note who played their first NHL game in 1965–66 (listed with their first team, asterisk(*) marks debut in playoffs):
 * J. P. Parise, Boston Bruins
 * Derek Sanderson, Boston Bruins
 * Bernie Parent, Boston Bruins
 * Barry Ashbee, Boston Bruins
 * Pete Mahovlich, Detroit Red Wings
 * Danny Grant, Montreal Canadiens
 * Ed Giacomin, New York Rangers

Last games
The following is a list of players of note that played their last game in the NHL in 1965–66 (listed with their last team):
 * Bill Gadsby, Detroit Red Wings

Broadcasting
Hockey Night in Canada on CBC Television televised Saturday night regular season games and Stanley Cup playoff games. HNIC also began producing Wednesday night regular season game telecasts for CTV. Games were typically not broadcast in their entirety until the 1968–69 season, and were typically joined in progress.

NBC agreed to air 1966 Sunday afternoon playoff games, marking the first time since the 1959–60 season that the NHL aired nationally in the U.S., and the first time ever that postseason games aired on American network television. The clinching Game 6 of the 1966 Stanley Cup Finals on Thursday, May 5 aired across RKO General-owned stations.

title: 1965–66 NHL season


text:
Talk:Spectre of the Gun

Peace
(rv in the NPOV ideal ...of making peace with another who cares about Star Trek as well I do, and in the selfless interest of intergalactic peace sometimes one just has to do "the greater good" thing.) (Cathytreks 17:03, 26 August 2005 (UTC))

Futurama?
Would it be worth mentioning this setting 'reappears' on an episode of Futurama? I wouldn't normally care about such cultural references but most of the cast does voices for the Futurama episode in question. Lots42 15:56, 14 September 2007 (UTC)

 * Agreed, put it in. 13:26, 12 April 2023 (UTC) 2A02:3035:414:82AD:78BD:50B2:9798:7C58 (talk) 13:26, 12 April 2023 (UTC)

DeForest Kelly Film Appearance
I see the Deforest Kelly film appearance has been added and removed before, apologies if it's been deemed irrelevant. WaltTFB (talk) 21:01, 22 June 2010 (UTC)
 * More trivia than completely irrelevant. WikiuserNI (talk) 09:14, 23 June 2010 (UTC)

Hour of the Gun
The title of this 1968 episode is likely a reference to the 1967 film Hour of the Gun, starring James Garner and Jason Robards. This is probably too trivial for inclusion in either article, though, and I have not yet found any citable references to support this. — Loadmaster (talk) 17:59, 17 December 2012 (UTC)

 * To add a little background/trivia, DeForest Kelley was originally cast for the role of Morgan Earp in the film, but could not perform the part since he was then engaged with Paramount for Star Trek (see IMDB). — Loadmaster (talk) 00:52, 30 April 2013 (UTC)

title: Talk:Spectre of the Gun


text: User talk:70.22.245.166

title: User talk:70.22.245.166


text: User talk:204.228.23.141

title: User talk:204.228.23.141


text:
SBK: Snowboard Kids

SBK: Snowboard Kids, released in Japan as Snowboard Kids Party (スノボキッズパーティー), is a snowboarding video game for the Nintendo DS released on November 2005 in North America and Japan. It was also released in Europe on April 28, 2006. It is the third and final game in the Snowboard Kids series. Up to four people can play wirelessly with one game card.

Characters
The game consists of characters Slash Kamei, Brad Maltinie, Nancy Neil, Jamjars "Jam" Kuehnemund, Koyuki Tanaka, Thomas "Tommy" Parsy, and Max. Jack Frost, mascot of Atlus and demon in the Megami Tensei series, makes an appearance as a hidden character. Black Frost is a more sinister looking version of Jack Frost with better stats.

Linda Maltinie, the character responsible for starting most of the competitions in the previous Snowboard Kids games, is absent and has replaced by Brad.

The characters' super deformed, large-nosed style has been discontinued, and in this game the characters take on an appearance that is much more standard and anime-esque. Some of the characters have undergone drastic personality changes, the two most noticeable being Nancy and Tommy. They were both mild-mannered, nice to everyone and kind but now, have become mean-spirited and even borderline antagonistic.

Reception
SBK: Snowboard Kids received "mixed" reviews according to the review aggregation website Metacritic.

GameSpot praised the game for its lengthy courses and being like an SSX and Mario Kart mix, but criticized it for having less personality than the previous two games in the series. IGN also praised the game for the time trials and the slalom missions, yet criticized it for its lack of focus on real arcade racing balance. Nintendo Power, however, called it "Mario Kart on ice." In Japan, Famitsu gave it a score of one eight, two sevens, and one six for a total of 28 out of 40, while Famitsu Cube + Advance also gave it all four sevens for a total of 28 out of 40.

title: SBK: Snowboard Kids


text:
Heyting arithmetic

In mathematical logic, Heyting arithmetic $${\mathsf{HA}}$$ is an axiomatization of arithmetic in accordance with the philosophy of intuitionism. It is named after Arend Heyting, who first proposed it.

Axiomatization
Heyting arithmetic can be characterized just like the first-order theory of Peano arithmetic $${\mathsf{PA}}$$, except that it uses the intuitionistic predicate calculus $${\mathsf{IQC}}$$ for inference. In particular, this means that the double-negation elimination principle, as well as the principle of the excluded middle $${\mathrm{PEM}}$$, do not hold. Note that to say $${\mathrm{PEM}}$$ does not hold exactly means that the excluded middle statement is not automatically provable for all propositions—indeed many such statements are still provable in $${\mathsf{HA}}$$ and the negation of any such disjunction is inconsistent. $${\mathsf{PA}}$$ is strictly stronger than $${\mathsf{HA}}$$ in the sense that all $${\mathsf{HA}}$$-theorems are also $${\mathsf{PA}}$$-theorems.

Heyting arithmetic comprises the axioms of Peano arithmetic and the intended model is the collection of natural numbers $${\mathbb N}$$. The signature includes zero "$$0$$" and the successor "$$S$$", and the theories characterize addition and multiplication. This impacts the logic: With $$1:=S0$$, it is a metatheorem that $$\bot$$ can be defined as $$0=1$$ and so that $$\neg P$$ is $$P\to\bot$$ for every proposition $$P$$. The negation of $$\bot$$ is of the form $$P\to P$$ and thus a trivial proposition.

For terms, write $$s\neq t$$ for $$\neg(s= t)$$. For a fixed term $$t$$, the equality $$t=t$$ is true by reflexivity and a proposition $$P$$ is equivalent to $$(t=t)\to P$$. It may be shown that $$P\lor Q$$ can then be defined as $$\exists n. (n=0\to P)\land(n\neq 0\to Q)$$. This formal elimination of disjunctions was not possible in the quantifier-free primitive recursive arithmetic $${\mathsf{PRA}}$$. The theory may be extended with function symbols for any primitive recursive function, making $${\mathsf{PRA}}$$ also a fragment of this theory. For a total function $$f$$, one often considers predicates of the form $$f(n)=0$$.

Double negations
With explosion valid in any intuitionistic theory, if $$\neg\neg P$$ is a theorem for some $$P$$, then by definition $$\neg P$$ is provable if and only if the theory is inconsistent. Indeed, in Heyting arithmetic the double-negation explicitly expresses $$\neg P\to 0=1$$. For a predicate $$Q$$, a theorem of the form $$\neg\neg \exists n. Q(n)$$ expresses that it is inconsistent to rule out that $$Q(t)$$ could be validated for some $$t$$. Constructively, this is weaker than the existence claim of such a $$t$$. A big part of the metatheoretical discussion will concern classically provable existence claims.

A double-negation $$\neg\neg P$$ entails $$(\alpha\to\neg P)\to(\alpha\to 0=1)$$. So a theorem of the form $$\neg\neg P$$ also always gives new means to conclusively reject (also positive) statements $$\alpha$$.

Proofs of classically equivalent statements
Recall that the implication in $$\mathsf{HA}\vdash\alpha\to\neg\neg\alpha$$ can classically be reversed, and with that so can the one in $$\mathsf{HA}\vdash\big(\exists n. \neg \psi(n)\big) \to \neg\forall n. \psi(n)$$. Here the distinction is between existence of numerical counter-examples versus absurd conclusions when assuming validity for all numbers. Inserting double-negations turns $${\mathsf{PA}}$$-theorems into $${\mathsf{HA}}$$-theorems. More exactly, for any formula provable in $${\mathsf{PA}}$$, the classically equivalent Gödel–Gentzen negative translation of that formula is already provable in $${\mathsf{HA}}$$. In one formulation, the translation procedure includes a rewriting of $$\big(\exists n. Q(n)\big)^N$$ to $$\neg\forall n.\neg Q^N(n).$$ The result means that all Peano arithmetic theorems have a proof that consists of a constructive proof followed by a classical logical rewriting. Roughly, the final step amounts to applications of double-negation elimination.

In particular, with undecidable atomic propositions being absent, for any proposition $$\psi$$ not including existential quantifications or disjunctions at all, one has $${\mathsf{PA}}\vdash\psi \iff {\mathsf{HA}}\vdash \psi$$.

Valid principles and rules
Minimal logic proves double-negation elimination for negated formulas, $$\neg\neg(\neg\alpha)\leftrightarrow(\neg\alpha)$$. More generally, Heyting arithmetic proves this classical equivalence for any Harrop formula.

And $$\Sigma_1^0$$-results are well behaved as well: Markov's rule at the lowest level of the arithmetical hierarchy is an admissible rule of inference, i.e. for $$\varphi$$ with $$n$$ free,
 * $${\mathsf{HA}}\vdash \neg\neg\exists m. \varphi(n, m)\iff {\mathsf{HA}}\vdash \exists m. \varphi(n, m)$$

Instead of speaking of quantifier-free predicates, one may equivalently formulate this for primitive recursive predicate or Kleene's T predicate, called $${\mathrm{MR}}_\mathrm{QF}$$, resp. $${\mathrm{MR}_\mathrm{PR}}$$ and $${\mathrm{MR}_0}$$. Even the related rule $${\mathrm{MR}}_\mathrm{Dec}$$ is admissible, in which the tractability aspect of $$\varphi$$ is not e.g. based on a syntactic condition but where the left hand side also requires $$\vdash \forall m.\varphi(n, m)\lor \neg\varphi(n, m)$$.

Beware that in classifying a proposition based on its syntactic form, one ought not mistakenly assign a lower complexity based on some only classical valid equivalence.

Excluded middle
As with other theories over intuitionistic logic, various instances of $${\mathrm{PEM}}$$ can be proven in this constructive arithmetic. By disjunction introduction, whenever either the proposition $$P$$ or $$\neg P$$ is proven, then $$P\lor\neg P$$ is proven as well. So for example, equipped with $$0=0$$ and $$\forall n. Sn\neq 0$$ from the axioms, one may validate the premise for induction of excluded middle for the predicate $$n=0$$. One then says equality to zero is decidable. Indeed, $${\mathsf{HA}}$$ proves equality "$$=$$" decidable for all numbers, i.e. $$\forall n. \forall m. (n = m\lor n \neq m)$$. Stronger yet, as equality is the only predicate symbol in Heyting arithmetic, it then follows that, for any quantifier-free formula $$\phi$$, where $$n,\dots,m$$ are the free variables, the theory is closed under the rule
 * $${\mathsf{HA}}\vdash \forall n. \cdots \forall m.\,\phi(n, \dots, m)\lor\neg\phi(n, \dots, m)$$

Any theory over minimal logic proves $$\neg\neg(P\lor \neg P)$$ for all propositions. So if the theory is consistent, it never proves the negation of an excluded middle statement.

Practically speaking, in rather conservative constructive frameworks such as $${\mathsf{HA}}$$, when it is understood what type of statements are algorithmically decidable, then an unprovability result of an excluded middle disjunction expresses the algorithmic undecidability of $$P$$.

Conservativity
For simple statements, the theory does not just validate such classically valid binary dichotomies $$\phi(n,\dots)\lor\neg\phi(n,\dots)$$. The Friedman translation can be used to establish that $${\mathsf{PA}}$$'s $$\Pi_2^0$$-theorems are all proven by $${\mathsf{HA}}$$: For any $$n$$ and quantifier-free $$\varphi$$,
 * $${\mathsf{PA}}\vdash \exists m. \varphi(n, m)\iff {\mathsf{HA}}\vdash \exists m. \varphi(n, m)$$

This result may of course also be expressed with explicit universal closures $$\forall n$$. Roughly, simple statements about computable relations provable classically are already provable constructively. Although in halting problems, not just quantifier-free propositions but also $$\Pi_1^0$$-propositions play an important role, and as will be argued these can be even classically independent. Similarly, already unique existence $$\exists!n. Q(n)$$ in an infinite domain, i.e. $$\exists n. \forall w. \big(n=w \leftrightarrow Q(w)\big)$$, is formally not particularly simple.

So $${\mathsf{PA}}$$ is $$\Pi_2^0$$-conservative over $${\mathsf{HA}}$$. For contrast, while the classical theory of Robinson arithmetic $${\mathsf{Q}}$$ proves all $$\Sigma_1^0$$-$${\mathsf{PA}}$$-theorems, some simple $$\Pi_1^0$$-$${\mathsf{PA}}$$-theorems are independent of it. Induction also plays a crucial role in Friedman's result: For example, the more workable theory obtained by strengthening $${\mathsf{Q}}$$ with axioms about ordering, and optionally decidable equality, does prove more $$\Pi_2^0$$-statements than its intuitionistic counterpart.

The discussion here is by no means exhaustive. There are various results for when a classical theorem is already entailed by the constructive theory. Also note that it can be relevant what logic was used to obtain metalogical results. For example, many results on realizability were indeed obtained in a constructive metalogic. But when no specific context is given, stated results need to be assumed to be classical.

Unprovable statements
Independence results concern propositions such that neither they, nor their negations can be proven in a theory. If the classical theory is consistent (i.e. does not prove $$\bot$$) and the constructive counterpart does not prove one of its classical theorems $$P$$, then that $$P$$ is independent of the latter. Given some independent propositions, it is easy to define more from them, especially in a constructive framework.

Heyting arithmetic has the disjunction property $${\mathrm{DP}}$$: For all propositions $$ \alpha $$ and $$ \beta $$,
 * $${\mathsf{HA}}\vdash\alpha\lor\beta\iff{\mathsf{HA}}\vdash\alpha\text{ or }{\mathsf{HA}}\vdash\beta$$

Indeed, this and its numerical generalization are also exhibited by constructive second-order arithmetic and common set theories such as $${\mathsf{CZF}}$$ and $${\mathsf{IZF}}$$. It is a common desideratum for the informal notion of a constructive theory. Now in a theory with $${\mathrm{DP}}$$, if a proposition $$P$$ is independent, then the classically trivial $$P\lor \neg P$$ is another independent proposition, and vice versa. A schema is not valid if there is at least one instance that cannot be proven, which is how $${\mathrm{PEM}}$$ comes to fail. One may break $${\mathrm{DP}}$$ by adopting an excluded middle statement axiomatically without validating either of the disjuncts, as is the case in $${\mathsf{PA}}$$.

More can be said: If $$P$$ is even classically independent, then also the negation $$\neg P$$ is independent—this holds whether or not $$\neg\neg P$$ is equivalent to $$P$$. Then, constructively, the weak excluded middle $${\mathrm{WPEM}}$$ does not hold, i.e. the principle that $$\neg\alpha\lor\neg\neg\alpha$$ would hold for all propositions is not valid. If such $$P$$ is $$\Sigma_1^0$$, unprovability of the disjunction manifests the breakdown of $$\Pi_1^0$$-$${\mathrm{PEM}}$$, or what amounts to an instance of ${\mathrm{WLPO}}$ for a primitive recursive function.

Classically independent propositions
Knowledge of Gödel's incompleteness theorems aids in understanding the type of statements that are $${\mathsf{PA}}$$-provable but not $${\mathsf{HA}}$$-provable.

The resolution of Hilbert's tenth problem provided some concrete polynomials $$f$$ and corresponding polynomial equations, such that the claim that the latter have a solution is algorithmically undecidable. The proposition can be expressed as
 * $$\exists w_1.\cdots\exists w_n. f(w_1, \dots, w_n)=0$$

Certain such zero value existence claims have a more particular interpretation: Theories such as $${\mathsf{PA}}$$ or $${\mathsf{ZFC}}$$ prove that these propositions are equivalent to the arithmetized claim of the theories own inconsistency. Thus, such propositions can even be written down for strong classical set theories.

In a consistent and sound arithmetic theory, such an existence claim $${\mathrm{I}_f}$$ is an independent $$\Sigma_1^0$$-proposition. Then $${\mathrm{C}_f}:=\neg {\mathrm{I}_f}$$, by pushing a negation through the quantifier, is seen to be an independent Goldbach-type- or $$\Pi_1^0$$-proposition. To be explicit, the double-negation $$\neg\neg{\mathrm{I}_f}$$ (or $$\neg{\mathrm{C}_f}$$) is also independent. And any triple-negation is, in any case, already intuitionistically equivalent to a single negation.

PA violates DP
The following illuminates the meaning involved in such independent statements. Given an index in an enumeration of all proofs of a theory, one can inspect what proposition it is a proof of. $${\mathsf{PA}}$$ is adequate in that it can correctly represent this procedure: there is a primitive recursive predicate $$\mathrm{F}(w):=\mathrm{Prf}(w, \ulcorner 0=1 \urcorner)$$ expressing that a proof is one of the absurd proposition $$0=1$$. This relates to the more explicitly arithmetical predicate above, about a polynomial's return value being zero. One may metalogically reason that if $${\mathsf{PA}}$$ is consistent, then it indeed proves $$\neg\mathrm{F}({\underline{\mathrm w}})$$ for every individual index $${\mathrm w}$$.

In an effectively axiomatized theory, one may successively perform an inspection of each proof. If a theory is indeed consistent, then there does not exist a proof of an absurdity, which corresponds to the statement that the mentioned "absurdity search" will never halt. Formally in the theory, the former is expressed by the proposition $$\neg\exists w. \mathrm{F}(w)$$, negating the arithmetized inconsistency claim. The equivalent $$\Pi_1^0$$-proposition $$\forall w. \neg \mathrm{F}(w)$$ formalizes the never halting of the search by stating that all proofs are not a proof of an absurdity. And indeed, in an omega-consistent theory that accurately represents provability, there is no proof that the absurdity search would ever conclude by halting (explicit inconsistency not derivable), nor—as shown by Gödel—can there be a proof that the absurdity search would never halt (consistency not derivable). Reformulated, there is no proof that the absurdity search never halts (consistency not derivable), nor is there a proof that the absurdity search does not never halt (consistency not rejectible). To reiterate, neither of these two disjuncts is $${\mathsf{PA}}$$-provable, while their disjunction is trivially $${\mathsf{PA}}$$-provable. Indeed, if $${\mathsf{PA}}$$ is consistent then it violates $${\mathrm{DP}}$$.

The $$\Sigma_1^0$$-proposition expressing the existence of a proof of $$0=1$$ is a logically positive statement. Nonetheless, it is historically denoted $$\neg{\mathrm{Con}}_{\mathsf{PA}}$$, while its negation is a $$\Pi_1^0$$-proposition denoted by $${\mathrm{Con}}_{\mathsf{PA}}$$. In a constructive context, this use of the negation sign may be misleading nomenclature.

Friedman established another interesting unprovable statement, namely that a consistent and adequate theory never proves its arithmetized disjunction property.

Unprovable classical principles
Already minimal logic logically proves all non-contradiction claims, and in particular $$\neg({\mathrm{I}_f}\land\neg{\mathrm{I}_f})$$ and $$\neg({\mathrm{C}_f}\land\neg{\mathrm{C}_f})$$. Since also $$({\mathrm{C}_f}\land\neg{\mathrm{C}_f})\leftrightarrow\neg({\mathrm{I}_f}\lor\neg{\mathrm{I}_f})$$, the theorem $$\neg({\mathrm{C}_f}\land\neg{\mathrm{C}_f})$$ may be read as a provable double-negated excluded middle disjunction (or existence claim). But in light of the disjunction property, or since the one relevant De Morgan's law does not hold intuitionistically, the plain excluded middle $${\mathrm{C}_f}\lor\neg{\mathrm{C}_f}$$ cannot be $${\mathsf{HA}}$$-provable.

The breakdown of the principles $${\mathrm{WPEM}}$$ and $${\mathrm{WLPO}}$$ have been explained. Now in $${\mathsf{PA}}$$, the least number principle $${\mathrm{LNP}}$$ is just one of many statements equivalent to the induction principle. The proof below shows how $${\mathrm{LNP}}$$ implies $${\mathrm{PEM}}$$, and therefore why this principle also cannot be generally valid in $${\mathsf{HA}}$$. However, the schema granting double-negated least number existence for every non-trivial predicate, denoted $$\neg\neg{\mathrm{LNP}}$$, is generally valid. In light of Gödel's proof, the breakdown of these three principles can be understood as Heyting arithmetic being consistent with the provability reading of constructive logic.

Markov's principle for primitive recursive predicates $${\mathrm{MP}_\mathrm{PR}}$$ does already not hold as an implication schema for $${\mathsf{HA}}$$, let alone the strictly stronger $${\mathrm{MP}_\mathrm{Dec}}$$. Although in the form of the corresponding rules, they are admissible, as mentioned. Similarly, the theory does not prove the independence of premise principle $${\mathrm{IP}}$$ for negated predicates, albeit it is closed under the rule for all negated propositions, i.e. one may pull out the existential quantifier in $$\neg P\to\exists n.Q(n)$$. The same holds for the version where the existential statement is replaced by a mere disjunction.

The valid implication $$\neg\neg(\alpha\to\beta)\to(\alpha\to\neg\neg\beta)$$ can be proven to hold also in its reversed form, using the disjunctive syllogism. However, the double-negation shift $${\mathrm{DNS}}$$ is not intuitionistically provable, i.e. the schema of commutativity of "$$\neg\neg$$" with universal quantification over all numbers. This is an interesting breakdown that is explained by the consistency of $$\neg{\mathrm{Dec}_M}$$ for some $$M$$, as discussed in the section on Church's thesis.

Least number principle
Making use of the order relation on the naturals, the strong induction principle reads
 * $$\forall n. \Big(\big(\forall (k < n). \phi(k)\big)\,\to\, \phi(n)\Big)\,\to\,\forall m. \phi(m)$$

In class notation, as familiar from set theory, an arithmetic statement $$Q(n)$$ is expressed as $$n\in B$$ where $$B:=\{m\in{\mathbb N}\mid Q(m)\}$$. For any given predicate of negated form, i.e. $$\phi(n):=\neg(n\in B)$$, a logical equivalent to induction is
 * $$\neg\exists (n\in B). \neg\exists (k\in B). k < n \,\,\,\leftrightarrow\,\,\, B=\{\}$$

The insight is that among subclasses $$B\subseteq{\mathbb N}$$, the property of (provably) having no least member is equivalent to being uninhabited, i.e. to being the empty class. Taking the contrapositive results in a theorem expressing that for any non-empty subclass, it cannot consistently be ruled out that there exists a member $$n\in B$$ such that there is no member $$k\in B$$ smaller than $$n$$:
 * $$B\neq\{\} \,\to\, \neg\neg\exists (n\in B). \neg\exists (k\in B). k < n$$

In Peano arithmetic, where double-negation elimination is always valid, this proves the least number principle in its common formulation. In the classical reading, being non-empty is equivalent to (provably) being inhabited by some least member.

A binary relation "$$ < $$" that validates the strong induction schema in the above form is always also irreflexive: Considering $$\phi_c(n):=(n\neq c)$$ or equivalently
 * $$Q_c(n):=(n=c)$$

for some fixed number $$c$$, the above simplifies to the statement that no member $$k$$ of $$B=\{c\}$$ validates $$k<c$$, which is to say $$\neg(c<c)$$. (And this logical deduction did not even use any other property of the binary relation.) More generally, if $$B$$ is non-empty and the associated (classical) least number principle can be used to prove some statement of negated form (such as $$\neg(c<c)$$), then one can extend this to a fully constructive proof. This is because implications $$\alpha\to\neg\beta$$ are always intutionistically equivalent to the formally stronger $$(\neg\neg\alpha)\to\neg\beta$$.

But in general, over constructive logic, the weakening of the least number principle can not be lifted. The following example demonstrates this: For some proposition $$P$$ (say $${\mathrm{C}_f}$$ as above), consider the predicate
 * $$Q_P(n) := (n=0\land P)\lor(n=1)$$

This $$Q_P$$ corresponds to a subclass $$b_P:=\{z\in\{0\}\mid P\}\cup\{1\}$$ of the natural numbers. One may ask what the least member of this class may be. Any number proven or assumed to be in this class provably either equals $$0$$ or $$1$$, i.e. $$b_P\subseteq\{0,1\}$$. Using decidability of equality and the disjunctive syllogism proves the equivalence $$P\leftrightarrow Q_P(0)$$. If the underlying proposition $$P$$ is independent, then the predicate is undecidable in the theory. Now since $$1=1$$, the proposition $$Q_P(1)$$ is trivially true and so the class is inhabited: $$1\in b_P$$. In particular, least number existence for this class cannot be rejected. Given a conjunction with $$Q_P(1)$$ is trivial, the existence claim of a least number validating $$Q_P$$ itself translates to the excluded middle statement for $$P$$. Knowledge of such a number's value in fact determines whether or not $$P$$ holds. So for independent $$P$$, the least number principle instance with $$Q_P$$ is also independent of $${\mathsf{HA}}$$.

In set theory notation, $$P$$ is equivalent to $$0\in b_P$$ and so $$b_P=\{0,1\}$$, while its negation is also equivalent to $$b_P=\{1\}$$. This demonstrates that elusive predicates can define elusive subsets. And so also in constructive set theory, while the standard order on the class of naturals is decidable, the naturals are not well-ordered. But strong induction principles, that constructively do not imply unrealizable existence claims, are also still available.

Anti-classical extensions
In a computable context, for a predicate $$M$$, the classically trivial infinite disjunction
 * $$\forall n.\big(M(n)\lor\neg M(n)\big)$$,

also written $${\mathrm{Dec}}_M$$, can be read as a validation of the decidability of a decision problem. In class notation, $$M(n)$$ is also written $$n\in M$$.

$${\mathsf{HA}}$$ proves no propositions not provable by $${\mathsf{PA}}$$ and so, in particular, it does not reject any theorems of the classical theory. But there are also predicates $$M$$ such that the axioms $${\mathsf{HA}}+\neg{\mathrm{Dec}}_M$$ are consistent. Again, constructively, such a negation is not equivalent to the existence of a particular numerical counter-example $$t$$ to excluded middle for $$M(t)$$. Indeed, already minimal logic proves the double-negated excluded middle for all propositions, and so $$\forall n. \neg\neg\big( Q(n)\lor\neg Q(n) \big)$$, which is equivalent to $$\neg\exists n.\neg\big( Q(n)\lor\neg Q(n) \big)$$, for any predicate $$Q$$.

Church's thesis
Church's rule is an admissible rule in $${\mathsf{HA}}$$. Church's thesis principle $${\mathrm{CT}_0}$$ may be adopted in $${\mathsf{HA}}$$, while $${\mathsf{PA}}$$ rejects it: It implies negations such as the ones just described.

Consider the principle in the form stating that all predicates that are decidable in the logic sense above are also decidable by a total computable function. To see how it is in conflict with excluded middle, one merely needs to define a predicate that is not computably decidable. To this end, write $$\Delta_e(w):=T_1(e, e, w)$$ for predicates defined from Kleene's T predicate. The indices $$e$$ of total computable functions fulfill $$\forall x. \exists w. T_1(e, x, w)$$. While $$T_1$$ can be realized in a primitive recursive fashion, the predicate $$\exists w. \Delta_e(w)$$ in $$e$$, i.e. the class $$H:=\{e\mid \exists w. \Delta_e(w)\}$$ of partial computable function indices with a witness describing how they halt on the diagonal, is computably enumerable but not computable. The classical compliment $$M$$ defined using $$\neg\exists w. \Delta_e(w)$$ is not even computably enumerable, see halting problem. This provenly undecidable problem $$e\in M$$ provides a violating example. For any index $$e$$, the equivalent form $$\forall w. \neg \Delta_e(w)$$ expresses that when the corresponding function is evaluated (at $$e$$), then all conceivable descriptions of evaluation histories ($$w$$) do not describe the evaluation at hand. Specifically, this not being decidable for functions establishes the negation of what amounts to $${\mathrm{WLPO}}$$.

The formal Church's principles are associated with the recursive school, naturally. Markov's principle $${\mathrm{MP}_\mathrm{Dec}}$$ is commonly adopted, by that school and by constructive mathematics more broadly. In the presence of Church's principle, $${\mathrm{MP}_\mathrm{Dec}}$$ is equivalent to its weaker form $${\mathrm{MP}_\mathrm{PR}}$$. The latter can generally be expressed as a single axiom, namely double-negation elimination for any $$\neg\neg\exists w. T_1(e, x, w)$$. Heyting arithmetic together with both $${\mathrm{MP}_\mathrm{Dec}}$$+$${\mathrm{ECT}_0}$$ prove independence of premise for decidable predicates, $${\mathrm{IP}}_0$$. But they do not go together, consistently, with $${\mathrm{IP}}$$. $${\mathrm{CT}_0}$$ also negates $${\mathrm{DNS}}$$. The intuitionist school of L. E. J. Brouwer extends Heyting arithmetic by a collection of principles that negate both $${\mathrm{PEM}}$$ as well as $${\mathrm{CT}_0}$$.

Consistency
If a theory is consistent, then no proof is one of an absurdity. Kurt Gödel introduced the negative translation and proved that if Heyting arithmetic is consistent, then so is Peano arithmetic. That is to say, he reduced the consistency task for $${\mathsf{PA}}$$ to that of $${\mathsf{HA}}$$. However, Gödel's incompleteness theorems, about the incapability of certain theories to prove their own consistency, also applies to Heyting arithmetic itself.

The standard model of the classical first-order theory $${\mathsf{PA}}$$ as well as any of its non-standard models is also a model for Heyting arithmetic $${\mathsf{HA}}$$.

Set theory
There are also constructive set theory models for full $${\mathsf{HA}}$$ and its intended semantics. Relatively weak set theories suffice: They shall adopt the Axiom of infinity, the Axiom schema of predicative separation to prove induction of arithmetical formulas in $$\omega$$, as well as the existence of function spaces on finite domains for recursive definitions. Specifically, those theories do not require $${\mathrm{PEM}}$$, the full axiom of separation or set induction (let alone the axiom of regularity), nor general function spaces (let alone the full axiom of power set).

$${\mathsf{HA}}$$ furthermore is bi-interpretable with a weak constructive set theory in which the class of ordinals is $$\omega$$, so that the collection of von Neumann naturals do not exist as a set in the theory. Meta-theoretically, the domain of that theory is as big as the class of its ordinals and essentially given through the class $${\mathrm{Fin}}$$ of all sets that are in bijection with a natural $$n\in\omega$$. As an axiom this is called $$V = {\mathrm{Fin}}$$ and the other axioms are those related to set algebra and order: Union and Binary Intersection, which is tightly related to the Predicative Separation schema, Extensionality, Pairing, and the Set induction schema. This theory is then already identical with the theory given by $${\mathsf{CZF}}$$ without Strong Infinity and with the finitude axiom added. The discussion of $${\mathsf{HA}}$$ in this set theory is as in model theory. And in the other direction, the set theoretical axioms are proven with respect to the primitive recursive relation
 * $$x\in y\iff \exists (r < 2^x). \exists (s < y). \big(2^x (2 s + 1)+ r = y\big)$$

That small universe of sets can be understood as the ordered collection of finite binary sequences which encode their mutual membership. For example, the $$ 100_2 $$'th set contains one other set and the $$ 110101_2 $$'th set contains four other sets. See BIT predicate.

Realizability
For some number $$\mathrm{n}$$ in the metatheory, the numeral in the studied object theory is denoted by $$\underline{\mathrm{n}}$$.

In intuitionistic arithmetics, the disjunction property $${\mathrm{DP}}$$ is typically valid. And it is a theorem that any c.e. extension of arithmetic for which it holds also has the numerical existence property $${\mathrm{NEP}}$$:
 * $${\mathsf{HA}}\vdash\exists n. \psi(n)\iff\text{ exists }{\mathrm{n}}\text{ }{\mathsf{HA}}\vdash\psi({\underline{\mathrm{n}}})$$

So these properties are metalogical equivalent in Heyting arithmetic. The existence and disjunction property in fact still holds when relativizing the existence claim by a Harrop formula $$\alpha$$, i.e. for provable $$\alpha\to\exists n. \psi(n)$$.

Kleene, a student of Church, introduced important realizability models of the Heyting arithmetic. In turn, his student Nels David Nelson established (in an extension of $${\mathsf{HA}}$$) that all closed theorems of $${\mathsf{HA}}$$ (meaning all variables are bound) can be realized. Inference in Heyting arithmetic preserves realizability. Moreover, if $${\mathsf{HA}}\vdash \forall n. \exists m. \varphi(n, m)$$ then there is a partial recursive function realizing $$\varphi$$ in the sense that whenever the function evaluated at $${\mathrm{n}}$$ terminates with $${\mathrm{m}}$$, then $${\mathsf{HA}}\vdash \varphi({\underline{\mathrm{n}}}, {\underline{\mathrm{m}}})$$. This can be extended to any finite number of function arguments $${\mathrm{n}}$$. There are also classical theorems that are not $${\mathsf{HA}}$$-provable but do have a realization.

Typed versions of realizability have been introduced by Georg Kreisel. With it he demonstrated the independence of the classically valid Markov's principle for intuitionistic theories.

See also BHK interpretation and Dialectica interpretation.

In the effective topos, already the finitely axiomizable subsystem of Heyting arithmetic with induction restricted to $$\Sigma_1$$ is categorical. Categoricity here is reminiscent of Tennenbaum's theorem. The model validates $${\mathsf{HA}}$$ but not $${\mathsf{PA}}$$ and so completeness fails in this context.

Type theory
Type theoretical realizations mirroring inference rules based logic formalizations have been implemented in various languages.

Extensions
Heyting arithmetic has been discussed with potential function symbols added for primitive recursive functions. That theory proves the Ackermann function total.

Beyond this, axiom and formalism selection always has been a debate even within the constructivist circle. Many typed extensions of $${\mathsf{HA}}$$ have been extensively studied in proof theory, e.g. with types of functions between numbers, and function between those, etc. The formalities naturally become more complicated, with different possible axioms governing the application of functions. The class of functions being total can be enriched this way. The theory with finite types $${\mathsf {HA}}^\omega$$ when further combined with function extensionality plus an axiom of choice in $${\mathbb N}^{\mathbb N}$$ still proves the same arithmetic formulas as just $${\mathsf {HA}}$$ and has a type theoretic interpretation. However, that theory rejects Church’s thesis for $${\mathbb N}^{\mathbb N}$$ as well as that all functions in $${\mathbb N}^{\mathbb N}\to {\mathbb N}$$ would be continuous. But adopting, say, different extensionality rules, choice axioms, Markov's and independence principles and even the Kőnig's lemma—all together but each at specific strength or levels—one can define rather "stuffed" arithmetics that may still fail to prove excluded middle at the level of $$\Pi_1^0$$-formulas. Early on, also variants with intensional equality and Brouwerian choice sequence have been investigated.

Reverse mathematics studies of constructive second-order arithmetic have been performed.

History
Formal axiomatization of the theory trace back to Heyting (1930), Herbrand and Kleene. Gödel proved the consistency result concerning $${\mathsf{PA}}$$ in 1933.

Related concepts
Heyting arithmetic should not be confused with Heyting algebras, which are the intuitionistic analogue of Boolean algebras.

title: Heyting arithmetic