Talk:Intuitionistic logic

comment by Charles Matthews

Very nice start to the article. A bit POV, though, it's kind of obvious it's written by an advocate of intuitionism. But still good start.

Ummm ... isn't it a bit narrow-based around the assumption of that old chestnut, intuitionism as one of the three main philosophies of mathematics? The Kolmogorov interpretation may have been the first step clear of that. Certainly the Brouwer not not not = not result needs a mention, too. Goedel used IL at one juncture, and after that, historically speaking, wasn't IL respectable in a technical sense? What happened then in relation to Markov was perhaps confusing.

Anyway, there are several strands to disentangle here: this is a bit ahistorical for me.

Charles Matthews 10:36, 15 Oct 2003 (UTC)

Agree on the history issue. For those into completeness, note that the Modal Logic "B" was intended to be a system matching Brouwer's intuition on "not". And that there are direct mappings between Intuitionist PC and the Modal Logic "S4" Nahaj 01:11:29, 2005-09-08 (UTC) And Ian Hacking pointed out in an early paper that there are validity preserving mappings between Intuitionist PC and the Modal Logic "S3" (A weaker system than S4). Nahaj 13:50, 26 October 2005 (UTC)

my take

Terms should not be equivocated. Speakers end up suggesting that not isn't not, so classical logicians should use a term meaning the exact opposite: un. lysdexia 00:16, 13 Nov 2004 (UTC)

I don't get it. How is this an example?

In the "law of the excluded middle" example under "Heyting algebra", $R^{2}$ is divvied up into a set A and its complement, the first comprising $\{(x,y):y>0\}$. Now, it would seem to me that the complement of A would be $\{(x,y):y\leq 0\}$. However, it's given as $\{(x,y):y<0\}$, which is then used to show that the $y=0$ plane isn't included in the union of A and not-A. How can this be? grendel|khan 03:45, 2005 Jan 14 (UTC)

It's really badly explained. But the idea is that if you consider subsets of $R^{2}$, they form a Heyting algebra if you consider "or" and "and" to be set union and intersection, and (this is they key point) the complement of X to be the interior of $R^{2}-X$. Then the complement of the open upper half-plane is the open lower half-plane. The axioms of the Heyting algebra are satisfied in this case, but the law that $X\vee \not X=R^{2}$ doesn't hold. -- Dominus 12:30, 14 Jan 2005 (UTC)

I've expanded the explanation (which I think still needs some more work) and included detailed examples of both a valid and and invalid formula. -- Dominus 16:19, 21 September 2005 (UTC)

There is no "third, indeterminate truth value"

The "Intuitionistic logic as a paradigm for logical reasoning" section presents a reasonably good overview of Intuitionism until we get to the third paragraph. Here we read a common misconception that, because Intuitionism rejects the law of the excluded middle, Intuitionistic logic supports a "third, indeterminate truth value".

Intuitionistic logic does not include any notion of a third truth value. Intuitionists do not believe that there is a formula P such that neither P nor ¬P is true. The reason why Intuitionistic logic rejects the law of the excluded middle has to do with their emphasis on provability. In Intuitionistic logic, the formula A ∨ B asserts that there is a either a proof of A, or there is a proof of B (or both). The law of the excluded middle, in Intuitionic terms, would therefore imply that there is a method by which, for any given formula P, we can generate a proof of either P or a proof of ¬P. Gödel's work dashed any hopes for such a method.

In short, the reason why Intuitionists reject the law of the excluded middle is not because there is a formula P which is neither true nor false. Intuitionists reject this law because there is no general algorithm which can determine which of the two truth values P has.

I move that we either replace or remove the third paragraph of "Intuitionistic logic as a paradigm for logical reasoning". -- Fatherbrain

I agree. I have removed that sentence, which was in the original revision of the article.

I would also like to remove the sentence that says "the validity of a mental construct is dependent upon its coherence with its context (the mind)." I've read this many times and I can't understand what is meant by it. -- Dominus 15:15, 21 September 2005 (UTC)

A similar oddity appears in the truth value article, which says:

A simple intuitionistic logic has truth values of true, false, and unknown

What does that mean? Should it also be removed? -- Dominus 13:26, 22 September 2005 (UTC)

Yes it should. Another correction to be made on this page is when Intuitionist formal logical calculus is contrasted with the "classical, two-valued case". In place of "two-valued", it should say "deterministic". -- FatherBrain 14:28, 22 September 2005 (UTC)

I've said more on this at Talk:truth value & similar changes should be applied here]]. — Charles Stewart (talk) 08:05, 25 June 2009 (UTC)

I've added a new para to the intro here, which I felt was still not totally clear to a reader who is unfamiliar with Intuitionistic logic - it could give the impression that it is an infinite valued logic. It also didn't explain how propositions are given a value of false in intuitionistic logic.

Unproved statements in Intuitionistic logic are not given an intermediate truth value (as is sometimes mistakenly asserted). Instead they remain of unknown truth value, until they are either proved or disproved. Statements are disproved by deducing a contradiction from them.

I've also edited the Truth value page - which had, at some point, had the sentence on intuitionistic logic removed, and have created a new section there on intuitinistic logic Robert Walker (talk) 07:11, 15 June 2014 (UTC)

Help me please

I am doing an assignment at the moment and it is very important that I do well. Can anybody give me a hand with it? I can email the questions otherwise can discuss them one at time here.

Cheers,

Does it say anywhere this is a wiki site, so obviously we help you cheat on your homework? Charles Matthews 07:16, 22 October 2005 (UTC)

And does it say anywhere in my request that I want someone else to do it for me? Sorry if I am not a naturally gifted legend like yourself Charles. You may be shocked to know that some of us have to work hard to get just an average grade and understanding doesn't just happen.

So if there is anyone who can assist me then I would be grateful.

Requests to deal privately by email are pretty suspect, you know. Charles Matthews 21:43, 22 October 2005 (UTC)

The only reason I suggested that was because then both parties would be looking at the same page and be able to discuss the questions much easier. Here is one for you then; I need to prove a theorem in intuitionistic propositional calculus, the question ask that you "indicate what axioms and inference rules" are used. I was under the impression that modus ponens was the only inference rule of intuitionistic calculus, however to procede with this proof "and elimination" would be handy. As the question refers to "inference rules" I was hoping I had missed something and there were more available to use.

Your thoughts?

Substitution is a rule of Intuitionist calculus (although not normally called an inference rule). While Modus Ponens is the basic inference rule of most calculi, most have a number of "derived rules" such as adjunction and substitution of equivalents. What counts as a rule needing to be given in your assignment depends on what your instructor has already given and what he has said. Obviously we don't know this. You could find therefore that an answer you get here (while in some sense "correct") is wrong for your assignment. Nahaj 21:03, 25 October 2005 (UTC)

There is an alternative to this: instead of a number of explicit axioms together with a substitution rule, one gives axiom schemes that determine an infinite set of individual axiom instances. Having a substitution rule is usual in modal logic, having axiom schemes seems most common elsewhere. --- Charles Stewart 21:22, 25 October 2005 (UTC)

Postscript: IIRC, Hilbert and Ackermann's Principles of Theoretical Logic uses axiom schemes. --- Charles Stewart 21:24, 25 October 2005 (UTC)

In the early days of Modal Logic, Axiom Schemata were VERY common. (And also rules like Adjunction, that were later proved to be derived rules in most systems of interest.) But by about the 1960's or so substitution had become more common in that field. In automated theorem proving substitution is more common, although a lot of recent automated work has used Condensed Detachment, which can be looked at as a (constrained) substitution followed by Modus Ponens. -- Nahaj 02:11, 30 October 2005 (UTC)

Not Not Not-p = Not-p?

Somebody mentioned aboved that this was a very fruitful result of Brouwer's. Which paper of Brouwer's discusses the importance of this fact in relation to intuitionist logic? (How does he argue it?) —Preceding unsigned comment added by 71.232.7.49 (talk • contribs) 00:41, July 23, 2006 (UTC)

Paradox of entailment

In the mathematical proof of the paradox of entailment I've seen, the axiom "if not not a then a" is used. Since this axiom doesn't exist in intuitionist logic, does that mean an inconsistency can arise without allowing every possible theorem, consistent or not, to be proved? If so, wouldn't this greatly decrease the problem in such a circumstance? Allowing some contradictions would allow certain metamathematical theorems such as Gödel's incompleteness theorems to be avoided. — Daniel 01:36, 5 June 2007 (UTC)

The logic that is usually called "intuitionistic logic" does have that property. Intuitionistic logic has an extra symbol $\bot$ which means false, and inference rules:

$\phi \land \lnot \phi \rightarrow \bot$

$\bot \rightarrow \psi$

From these, it follows immediately that if you have already shown $\phi \land \lnot \phi$ then you can infer $\psi$.

Another way of looking at the paradox of entailment is that it follows from the fact that $\phi \rightarrow (\lnot \phi \rightarrow \psi )$ is a tautology. That identity is also valid in intuitionistic logic, using the above inference rules. — Carl (CBM · talk) 01:50, 5 June 2007 (UTC)

Why'd they do that? They could have had a sufficiently complex complete logical system, but they just couldn't stand a contradiction. I don't see how it could do any good. It's better to have one contradiction then every one that could possibly be stated. By the way, why even have $\bot$? Why not just use $\psi$? It looks to me like they're equivalent and both mean "everything is true". I don't see how $\bot$ could mean false. You wouldn't say, "if false, Elvis is alive"; you would say, "if everything is true, Elvis is alive"… assuming you're the kind of guy who likes to state the obvious. Besides, I'm pretty sure $\bot$ means perpendicular. — Daniel 04:00, 5 June 2007 (UTC)

WikiProject class rating

This article was automatically assessed because at least one WikiProject had rated the article as start, and the rating on other projects was brought up to start class. BetacommandBot 04:08, 10 November 2007 (UTC)

Something wrong?

In the Heyting algebra section, it is stated that the values of intuitionist logic can be taken to be open sets, and later that negation is taking the exterior of the set. But then, the exterior of the exterior of an open set A is A itself; with the obvious muddle about negatives. —Preceding unsigned comment added by 92.50.68.238 (talk) 19:05, 10 March 2008 (UTC)

Your claim that ext(ext(S)) = S is mistaken. One can only show that ext(ext(S)) is a subset of S, but not conversely. Consider the set S = R - {(0,0)}. This is an open set. Then the exterior of S is empty, and the exterior of the empty set is not S but R. So we have a counterexample for $\neg \neg x\rightarrow x$. But because ext(ext(S)) is contained in S one can show that $x\rightarrow \neg \neg x$ does hold. -- Dominus (talk) 19:19, 10 March 2008 (UTC)

Actually it's the other way round (as your example shows): every open S is contained in ext(ext(S)), but ext(ext(S)) may be strictly larger than S. Indeed, ext(ext(S)) = S holds if and only if S is a regular open set. For a general open set S, ext(ext(S)) is its regularization. -- EJ (talk) 13:55, 11 March 2008 (UTC)

Ok, my mistake. Is there a logic that corresponds to regular open sets? —Preceding unsigned comment added by 81.210.250.222 (talk) 19:29, 28 March 2008 (UTC)

Yes, it is classical logic. -- EJ (talk) 10:54, 31 March 2008 (UTC)

I mean, a "logic that corresponds to regular open sets" can be understood in two different ways:

1. The logic of the algebra of regular open sets in a topological space. This is classical logic, as the algebra is Boolean. The join in this algebra is $A\lor B={\rm {int}}({\overline {A\cup B}})={\rm {ext}}({\rm {ext}}(A\cup B))$.
2. The "logic" obtained by evaluating propositional variables by regular open sets, but evaluating connectives as in intuitionistic logic. In this case, compound formulas may have nonregular sets as their value. This "logic" is not a logic at all, as it is not closed under substitution. It is the propositional intuitionistic theory axiomatized (over Int) by the formulas ¬¬p → p for all variables p. Equivalently, it can be described as the set of all formulas A(p₁,…,p_n) such that A(¬p₁,…,¬p_n) is an intuitionistic tautology. The logic of this theory (i.e., the set of formulas whose all substitution instances are theorems) is just intuitionistic logic. -- EJ (talk) 15:43, 31 March 2008 (UTC)

Heyting algebra of open subsets of R

What is a reference for the statement that the Heyting algebra of open subsets of R suffices for characterizing validity?  --Lambiam 14:04, 13 March 2008 (UTC)

The original paper is apparently

Alfred Tarski, Der Aussagenkalkül und die Topologie, Fundamenta Mathematicae 31 (1938), 103–134. [1]

In fact, he shows that intuitionistic logic is complete with respect to any second countable T₄ dense-in-itself space. I am not able to find an English reference ATM; there is a chance that it is in Rasiowa's and Sikorski's "Mathematics of Metamathematics". The more general result of completeness of S4 wrt the reals can be found here[2] for instance. -- EJ (talk) 15:00, 13 March 2008 (UTC)

Funny than you should ask this just now: I was going to add a cite for this yesterday, but then I got distracted while I was looking at [[3] and didn't finish. The fact can be supported with Sørensen and Urzyczyn's "Lectures on the Curry-Howard Isomorphism". I will try to hunt this up and add a reference today. -- Dominus (talk) 15:19, 13 March 2008 (UTC)

This is theorem 2.4.8 on page 33 of the lecture note version of Sørensen and Urzyczyn. A remark higher up on the same page asserts that "there is no single finite Heyting algebra [that is a sufficient model for intuitionistic logic]". Presumably the same assertions appear in but I don't have it handy just now. I will see if I can find a copy. -- Dominus (talk) 15:37, 13 March 2008 (UTC)

Sørensen and Urzyczyn cite Rasiowa and Sikorski. -- Dominus (talk) 15:40, 13 March 2008 (UTC)

The Penn library has but not . I've ordered the second from interlibrary services, and the first to be extracted from storage. I should be able to provide references some time next week. -- Dominus (talk) 15:54, 13 March 2008 (UTC)

I added an English reference, but, strangely, I was not able to find where it proved that no finite Heyting algebra is a model for the intuitionistic validity of all sentences. -- Dominus (talk) 17:06, 14 March 2008 (UTC)

In addition to the Tarski paper cited above, also cites the earlier paper . -- Dominus (talk) 17:02, 14 March 2008 (UTC)

The whole thing is now cited up down and backwards. -- Dominus (talk) 19:18, 18 March 2008 (UTC)

Can't read it

My browser is showing the syntax section as '... it is customary to use →, ∧, ∨, ⊥ as the basic connectives ...' and so on through the article. Never happened to me on Wikipedia before. Obviously, this makes the article completely unreadable. Any chance of fixing it? —Preceding unsigned comment added by 195.224.69.116 (talk) 16:07, 14 March 2008 (UTC)

Do you mean that you see little boxes instead of the actual symbols? — Carl (CBM · talk) 16:56, 14 March 2008 (UTC)

Yes —Preceding unsigned comment added by 195.224.69.116 (talk) 15:47, 9 April 2008 (UTC)

Which of these work for you:

$\land$ - ∧ - ∧

$\phi$ - φ - φ

— Carl (CBM · talk) 19:52, 10 April 2008 (UTC)

In the HTML produced for the page, the first wedge comes out as a png image, while the other two are both utf8 for Unicode Character 'LOGICAL AND' (U+2227). This should be the same for any viewer who has not set their Math rendering preference to "HTML if possible". The inability to see this should imply that also Logical connective#Order of precedence, for example, is totally unreadable.  --Lambiam 21:07, 11 April 2008 (UTC)

Verifiabilistic logic

Intuitionistic logic, or constructivist logic, is the symbolic logic system originally developed by Arend Heyting to provide a formal basis for Brouwer's programme of intuitionism.

Verifiabilistic logic, is the symbol not yet developed by anyone to provide a formal basis for wikipedias WP:V policy. (Just kidding!) 88.159.74.89 (talk) 15:14, 3 August 2009 (UTC)

`=' as Connective

I am not very familiar with intuitionistic logic, however, there seems to be a problem with the explanation of the syntax. Notice that `=' is used to define `¬' but `=' is not on the basic list of connectives. Either way, as an explanation for negation, using an undefined complex connective or a primitive but unlisted connective is not a good way to approach basic issues in syntax. I am not sure how to resolve this worry but it should be resolved. —Preceding unsigned comment added by 206.241.2.45 (talk) 17:43, 10 November 2009 (UTC)

You are misreading it. The "=" was merely denoting what is being defined by what, it is not part of the definition itself. It never ceases to fascinate me what things are people capable of misunderstanding. One would think that this one is completely obvious, since apart from its being a fairly standard notation, ¬ appeared on the left-hand side of the equality sign and couldn't possibly be part of definition of itself. — Emil J. 18:03, 10 November 2009 (UTC)

I rearranged the words, in any case, but I generally agree. — Carl (CBM · talk) 18:09, 10 November 2009 (UTC)

Ah, I missed the second occurrence. — Emil J. 18:15, 10 November 2009 (UTC)

Quantifier eleminiation

PRED-1: $(\forall x\ \phi (x))\to \phi (t)$, if no free occurrence of $x$ in $\phi$ is bound by a quantifier quantifying a variable occurring in the term $t$

Am I the only one for whom the condition does not even parse? I see how a variable that is free in one formula can be bound to a quantifier in another formula, but how can an occurance of one variable in a formula be bound in a term? Carsten Milkau (talk) 11:31, 27 September 2010 (UTC)

It was apparently trying to say "if no free occurrence of $x$ in $\phi$ is within the scope of a quantifier quantifying a variable occurring in the term $t$". I've replaced it with a more usual description.—Emil J. 12:38, 27 September 2010 (UTC)

if no occurrence of any variable in $t$ becomes bound in $\phi (t)$

This is a lot better, thank you very much! — Carsten Milkau (talk) 14:58, 27 September 2010 (UTC)

Again on the quantifier elimination

there's something I am not convinced in this:

$(\forall x\ \phi (x))\to \phi (t)$,  if the term $t$ is free for substitution for the variable $x$ in $\phi$ (i.e., if no occurrence of any variable in $t$ becomes bound in $\phi (t)$

Let's consider the sentence:

$\forall x\ (\forall y\ (x,y>0\to x+y>0))$ 

which is of the form $\forall x\ \phi (x).$ From my understanding of the definition, we cannot use the quantifier elimination axiom in this case to infer the sentence:

$\phi (y)=\forall y\ (y>0\to y+y>0)$ 

that is $\phi$ in which $x$ is substituted with $y$, because $y$ becomes bounded in $\phi (y)$. However, there seems to be nothing wrong with this inference to me... Maybe I didn't understand well the definition. I was thinking whether we could explain this better, maybe through some example. Enomisbomber (talk) 15:36, 18 February 2021 (UTC)

Heyting algebra semantics

I have a small question, maybe the answer could permit to clarify this article or the article Heyting algebra, or maybe I didn't think enough and my question is unfounded...

Thank you very much if someone can answer to this complicated question:

In this article, in "Heyting algebra semantics" part, it 's written:

• the value assigned to a formula A → B is int(A^C ∪ B)

So my question is why to use int(interor of a set)?

I base my question on the fact that in the article Heyting algebra a definition of A → B is :

• the greatest element x of H such that :$a\wedge x\leq b.$

And by this definition it seems to me that x doesn't need to be equal to int(A^C ∪ B) but instead (A^C ∪ B) is sufficient.

Indeed if for instance we take a = ] 2 ; 3 [ and b = [ 2 ; 3], then if we take x = (A^C ∪ B) (= ]-infinite;2] union [2;+infinite[)then we obtain the greatest x such that $a\wedge x\leq b.$, but if we take x = int(A^C ∪ B) it also works but x wouldn't be the greatest x as possible.

Am i doing an error or the two definitions of A → B in Intuitionistic logic article and in heyting algebra article contradicts them self?--Nicobzz (talk) 11:55, 22 December 2010 (UTC)

The discussion there is about a particular Heyting algebra, the algebra of open subsets of the real line. In general, if A and B are open subsets of R, then A^C ∪ B may not be an open set. For example let B be empty and let A be the interval (−∞,0), whose complement is the non-open set [0,∞).

So the function f(A,B) = A^C ∪ B does not always give an element of the algebra, since the only sets in the algebra are open sets. This means that f cannot be used to define an operation on the algebra. However, the function g(A,B) = int(A^C ∪ B) does always give an open set, and moreover there is a proof that this operation is compatible with the union and intersection operations so that it can be used to define an implication A→B on the algebra. — Carl (CBM · talk) 13:16, 22 December 2010 (UTC)

I'll say it in different words. The definition of A → B is indeed

the greatest element X of H such that $A\wedge X\leq B.$

However, H here is not the power set algebra, but the algebra of open sets, hence the definition translates to: the largest open set X such that $X\cap A\subseteq B$. This is equivalent to: the largest open set contained in $A^{C}\cup B$, and this is exactly $\operatorname {int} (A^{C}\cup B)$.—Emil J. 14:51, 22 December 2010 (UTC)

Thank you very much, in fact I didn't take care enough that we consider a single Heyting algebra whose elements are the open subsets of the real line R. And so, f(A,B) have to be $\operatorname {int} (A^{C}\cup B)$ to also belongs to the set of the open set of R. It's Clearer!--Nicobzz (talk) 11:17, 23 December 2010 (UTC)

One more classical identity is provable intuitionistically

In reference to the section on the non-interdefinability of the operators, I built a proof of the reverse direction of one of the identities that the article says is only provable in the forward direction. The identity in question is $\neg (\phi \to \psi )\leftarrow \neg (\neg \phi \vee \psi )$. I can't do it in the combinator-style axiomatization presented (because I got confused trying to eliminate the abstractions) but the proof term in the equivalent abstraction-style axiomatization is: $\lambda k^{\neg (\neg \phi \vee \psi )}.\lambda f^{\phi \to \psi }.k(\iota _{1}(\lambda a^{\phi }.k(\iota _{2}(fa))))$. Am I going insane here or is the article just mistaken? 209.51.184.11 (talk) 18:18, 9 October 2013 (UTC)

Intuitionistic provability of this implication follows immediately from Glivenko’s theorem. I’ll fix that.—Emil J. 11:12, 10 October 2013 (UTC)

On second thought, I don’t see the point of listed this separately in the first place. Any of the other identities becomes intuitionistically provable as well if one puts negation on both sides. There’s nothing remarkable about this fact, and it does not really express interdefinability of connectives.—Emil J. 11:17, 10 October 2013 (UTC)

Another relation to modal logic

Kurt Gödel showed (1993) that IL is equivalent to a modal logic with a modal operator B (for Beweisbar) that expresses the idea of provability. For example, Bp means that p is provable. Gödel set up axioms for B:

• Bp→(B(p→q)→Bq)
• Bp→p
• Bp→BBp

and then showed that with these axioms his system is equivalent to S4. He claimed that there is a bidirectional translation between statements in this logic and statements of IL, such that statements provable in this system are precisely the translations of theorems of IL; this claim was proved by Tarksi in 1948. This claim validates the usual BHK interpretation of IL.

Source: Goldblatt, Robert (2005). "Mathematical Modal Logic: a View of its Evolution". In Gabbay, Dov M.; Woods, John (eds.). Handbook of the History of Logic (PDF). Vol. 6. Elsevier. p. 8.

Tarski-like semantics

The claim "It was discovered that Tarski-like semantics for intuitionistic logic were not possible to prove complete." seems very confused to me. Semantics never is (are?) proved complete; theories are or are not proved complete. 86.132.222.147 (talk) 22:49, 19 November 2015 (UTC)

A logic is complete, relative to a class of models, if the statements provable in the logic are exactly the statements that hold in every model of the class. This is different than the sense of completeness of a theory (proving each sentence or its negation).

In classical logic, there is a standard way of doing semantics, but there are many deductive systems, so it is common to look at a completeness proof as showing that a deductive system is complete with respect to this standard semantics. On the other hand, intuitionistic logic is defined to some extent by a deductive system -- there is no "standard" way of doing intuitionistic semantics. So it is more common to view a completeness proof in intuitionistic logic as showing that a particular semantics is complete for the standard deductive system. — Carl (CBM · talk) 00:48, 20 November 2015 (UTC)

Intuitionistic vs Constructive

Also in this article intuitionistic and constructive seem to mean the same. However I would prefer to distinguish between those two notions:

1. Avoid the term constructive logic but use only intuitionistic logic
2. A mathematical theory is called intuitionistic if based on intuitionistic logic, e.g. Intuitionistic Zermelo–Fraenkel (IZF)
3. A mathematical theory is called constructive if based on intuitionistic logic and does not contain impredicative axioms, e.g. Constructive Zermelo–Fraenkel (CZF)

To summarise in a formula: constructive = intuitionistic + predicative

Please note that a predicative theory can be based on classical logic, e.g. Arithmetical transfinite recursion (ATR₀). Certainly not every theory can be precisely classified as predicative or impredicative as there is no precise definition of being predicative. The proof-theoretic ordinal can help to measure the degree of impredicativety, for which the notion of metapredicative has been introduced Kaelltee (talk) 13:00, 11 October 2017 (UTC)

I see the distinction you are making, but I am not sure it is common. I see "constructive logic" frequently enough. Some people use it in particular when they want to emphasize that they are not following Brouwer's philosophical campaign but only the logic that developed from it. Related to your third bullet, I am not sure I have ever seen that definition. Really there is no single definition of a "constructive theory" in my experience with the literature - different people use the term for different things, and disagree about whether particular theories are constructive. For example, some people admit as "constructive" theories that include Markov's principle, while others don't. The same goes for Church's thesis - is this a requirement of a constructive theory? — Carl (CBM · talk) 19:18, 11 October 2017 (UTC)

I agree that there is no precise definition of constructive. What the "right" definition of constructive is not the point of my comment. I just dislike the term constructive logic as synonym for intuitionistic logic because many logicians do not consider constructive to mean the same as intuitionistic.

For the term intuitionistic logic there is a wide agreement that it is bases on Brouwer's ideas, but just with divergent opinions on which extensions can be added.

If you want to use constructive in the sense of Bishop's Constructive Mathematics: When a man proves a positive integer to exist, he should show how to find it. If God has mathematics of his own that needs to be done, let him do it himself. (E.Bishop & D.Bridges:"Constructive Analysis", Springer-Verlag, 1985).

For that a proof of an existence statement may be called constructive it shall contain a method on how to construct a witness for the existence (and a proof that this witness satisfies the prperty). If you need the power set axiom of IZF to prove an existence then you will have a hard time to find an alghorithm providing a witness. That is why I do not want to call IZF constructive. Note that IZF has the same strength as ZF!

But I must admit that CZF is rather metapredicative than predicative as its proof-theortic strength is the Bachmann–Howard ordinal ψ(ε_{Ω+1}).

Church’s thesis is incompatible with Brouwer’s principle of continuous choice and the Fan Theorem and thus might not fit in Brouwers'world. Moreover many construcitve Mathematicians consider Markov's Principle as not acceptable, also because there is a Kripke Model showing that MP is not constructively derivable. For more details, have a look at http://www1.maths.leeds.ac.uk/~rathjen/book.pdf .Kaelltee (talk) 06:52, 12 October 2017 (UTC)

I came across this publication, quite in accord with Intuitionistism and Constructivism.

Mathematicians are continuously developing Maths. I am sure absurdity cannot be maths entirely!

"Even if Hilbert was not the first to give a non-constructive proof, he was a major proponent of the non-constructive spirit, especially in his early period. Although Kronecker, who in general influenced Hilbert34, believed that existential propositions are meaningless if they do not explicitly specify the object the existence of which they ascertain, Hilbert saw in the negation of PLE a major shrink of mathematics. Providing a constructive proof of his previously non-constructively proven basis theorem, he revealed the importance of PLE, since the object that had to be constructed was already proven to “exist”. Even Gordan admitted that “theology” had its merits. Of course, as we can already suspect from K¨onig’s lemma case, this cannot be done with every nonconstructively proven theorem..." http://www.math.lmu.de/~petrakis/Master%20Thesis.pdf .

"Though Brouwer was completely against mathematics with PLE, it is worth remarking that by ¬∃loxP(x) ⇒ ¬∃coxP(x), the proof of logical non-existence implies constructive non-existence. In that way constructively acceptable results of logical non-existence can be incorporated to a TK. There are two major, classical questions on the philosophy of mathematics..."

General concensus2012 (talk) 19:12, 21 September 2018 (UTC)

Constructive semantics

Constructive logic redirects to this article, which begs the question of why it doesn't mention the constructive perspective on the semantics (BHK interpretation or the like)? Like many other mathematicians, my main impression of intuitionistic logic used to be that it seemed to be a lot of sophistery about arbitrarily declaring some proof techniques as "unclean", but with little reason to the matter beyond "L. E. J. Brouwer said so," and the present state of the article doesn't do much to counter that impression.

• "Intuitionists don't like the Law of Excluded Middle? Well, since I happen to be taught to use a Hilbert-style deduction system which doesn't even have that as an explicit inference rule or axiom, this means nothing to me."
• "Intuitionistic logic gets its semantics from Heyting algebras? Well, since these seem to be defined specifically to match the intuitionistic logic (rather than the other way around), then why should I care? Why not rather do fuzzy logic, if the classical one seems too traditional?"

The first thing that gave me any hint that there really could be something here was precisely the constructive perspective: we exclude those proof techniques because they are not valid in the constructive interpretation. Therefore the article should, at least as motivation, present some variant of this interpretation. 130.243.68.105 (talk) 17:14, 26 November 2019 (UTC)

Intuitionistic Truth Operators

Hi. So I've read that in classical logic, you can basically define the binary logical operators with truth tables. (This may be an oversimplification, let me know if so) Assuming that is the case, can you do something similar with intuitionistic truth operators? That is, does each intuitionistic binary truth operator accept two arguments, each from a particular set of (the intuitionistic equivalent of) truth values, and output a particular value from the same set? Thanks for reading! JonathanHopeThisIsUnique (talk) 23:56, 1 February 2020 (UTC)

Definition of "law of excluded middle" in introduction

This page's introduction says

> In the semantics of classical logic, propositional formulae are assigned truth values from the two-element set ("true" and "false" respectively), regardless of whether we have direct evidence for either case. This is referred to as the 'law of excluded middle', because it excludes the possibility of any truth value besides 'true' or 'false'.

However, law of excluded middle is defined as (P or ~P) is true, not as there are only two truth values. Which page is correct? Wqwt (talk) 23:55, 19 September 2022 (UTC)