I’m incredibly busy right now adjusting to my new job and my new commute, which is leaving me less time than usual for blogging. So I’m going to raid the archives, and bring back some interesting things that appeared on the old Blogger blog, but were never posted here. As usual, that will involve some cleanups and rewrites, so this won’t be identical to the original posts.
I’ve written about logic before, and mentioned intuitionistic logic at least in passing. Intuitionistic logic is an interesting subject. Intuitionistic logic is a variation of predicate logic which is built on the idea that there should be a stronger notion of “truth” in logic: that the strict categorization of all statements in classical logic as either true or false is too strong. In intuitionistic logic, a statement is only true if you can prove that it is true. It is not enough to prove that it’s opposite is false: In propositional logic, it is not the case that ¬¬P→P.
In fact, truth is intuitionistic logic is defined by proof: A is true means that there exists a proof of A. A is false means that there is a proof that there is no proof of A. Most of the differences between intuitionistic and classical logic comes from that distinction between the classical meaning of true and false, and the intuitionistic meaning of true and false.
The intuitionistic meaning has the implication that many inferences that we’re used to in propositional logic are no longer valid in intuitionistic logic:
- In classical propositional logic, the statement “X∨¬X” is a tautology, which says that either X is true, or X is not true. In intuitionistic logic, it is not: the statement “X∨¬X” means that we can prove that either X is true or that X is false. X is true in intuitionistic logic if and only if we have a proof that X is true; X is false if and only if we can prove that there is no proof for X. If we do not have a proof for either the truth or the falsehood of X, then “X∨¬X” is not a true statement: it’s possible that X is true, but we don’t have a proof for it.
- In classical predicate logic, we can often infer statements like “∃ X : P(x)”, even though we don’t know what “x” is. In intuitionistic logic, to infer that statement, it must be possible to demonstrate at least one value for which it’s true. Similarly, in order to prove that a universal statement is false, we need to be able to show a concrete counterexample that demonstrates its falsehood. Intuitionistic logic is always constructive: proofs always generate concrete examples.
- In both propositional and intuitionistic logic, the statement that “P→¬¬P” is true. But in classical logic, “¬¬P -> P” is always true, but in intuitionistic logic, it is not. We can introduce double negation, but we can’t eliminate it: Since “not P” means “We can prove that there is no proof of P”, the fact that P is true (i.e., that we have a proof that P is true) means that we can prove that “not P” is false – because the fact that there is a proof for P provides a concrete counterexample to the statement that there is no proof for P – so “¬¬P”, which says “There is no proof that there is no proof for P” is proven true. But going the other direction: the fact that we can’t prove that there is no proof for P does not imply that there is a proof for P. In intuitionistic logic, being unable to prove that there is no proof for something is a much weaker statement that saying that that thing is true.
One way to think of intuitionistic logic is to think of it as if there were actually three values that can be assigned to a predicate: it can be in one of two definite states (proved true or proved false) or it can be in an indefinite state (unproven). If a predicate P is unproven, then we can assert neither that P is true nor that P is false. But if the predicate is in an indefinite state, and we can show a proof, then we can move it to a definite state: if we can find a way to provide a proof of P, then it becomes true; or if we can show that it’s unprovable, then it becomes false.
It’s worth reiterating: one of the really wonderful properties of intuitionistic logic is that it’s strongly constructionist. A proof that “¬A” in intuitionistic logic will always generate at least one concrete counterexample of A. There are entire programming languages built on this fundamental point. (Not to get too far off topic, but a prolog program basically works by negating a statement for which you want concrete examples, and then using intuitionistic inference to generate counterexamples for that negative – which are concrete examples of where the statement is true.)
The formal semantics of intuitionistic logic are more complicated than the semantics of predicate logic. They tend to involve things like lattice theory. In my next post, I’ll talk about one way of describing the semantics of intuitionistic logic called Kripke Semantics. Kripke semantics is useful not just for intuitionistic logic, but for a lot of other things, like temporal logics, modal logics, model checking – and providing models for many of the calculi that fascinate me. Kripke semantics provide the definitive model for λ-calculus, and by extension, for other fascinating calculi like the π-calculus.
Something I find counterintuitive in intuitionistic logic is the meaning “A or B is true”. This is unproblematic when you have a proof for A or a proof for B, but what if you introduce “A or B” as an axiom? (For example, let’s say you axiomatize the reals, and one of your axioms is “A B”.) It seems odd that “A or B” can be definitely known, while individually A and B are both in an indeterministic state.
If you have “A or B”, but don’t have either A or B, then your theory doesn’t make sense from the intuitionistic point of view. Similarly, if you have a proof “exists x such that A(x)” then there must be an actual a such that you can prove A(a).
“For example, let’s say you axiomatize the reals, and one of your axioms is “A (or?) B”.” What are A and B here?
Not only is it a partial rerun, it is a partial Basic post, no?
My tentative model (math sense) for intuitionist logic is observational facts. Then the above seem, well, intuitive, unless I am deluded.
Say for example that you have a model (practical sense – and possibly using predicate logic) or theory for some system where you can predict “A or B” for sure, which looks equivalent for me to your introducing it as an axiom. But you don’t know which it is until you measure.
The way to understand A∨B is that it’s a statement that you can prove A or you can prove B.
One of the nice things about intuitionistic logic is that its rules of inference are symmetric: You either introduce a construct or you eliminate it. There are two rules for introducing or:
A→A∨B
B→A∨B
So, for example, if you can prove A, you can prove A∨B.
If it helps, remember that you can inter-convert disjunction and implication, though the rules are not as simple as they are in classical logic.
Well, seems Alexey has an immediate counterexample showing why my model doesn’t work. Which still leaves me curious if there is a logic that models observations.
OR or XOR? I wasn’t completely sure about whether you meant your ‘v’s to be OR or XOR, since ‘v’ is usually standard OR, but you say “either … or”, which suggests XOR.
Oops, part of my comment got eaten (I used less than and greater than signs, which it took as malformed HTML tags.) I meant the trichotomy axiom: for any two reals A and B, either A is greater than B, A is less than B, or A is equal to B. The disjunction is true, even if you can’t prove anything about the relationship between A and B.
Walt: I thought it may have been what you meant.
The trychotomy axiom is incorrect intuitionistically for real numbers, precisely because we can construct two numbers A and B such that we can’t prove any part of the disjunction. It is correct for _rational_ numbers: given A=m/n and B=p/q we need just compare m*q and p*n.
I don’t think it is quite correct that ¬A means “you can prove that there is no proof of A”. I think I have read that intuitionistic logic with arithmetic satisfies Gõdel’s incompleteness theorem, so if that were true, you could never prove a negative statement, since you would have to prove that the theory is consistent.
From the derivation rules, my understanding is that ¬A rather means “you can prove everything from the assumption A”.
Orjan:
The usual interpretation of ¬A really is “there is no proof of A”. The intuitionistic logical is consistent, so there can clearly be tautologies of the form ¬A. Intuitionistic logic can also be formulated in terms of modal logic, and the “many worlds” interpretations of modal logic. Viewed that way, the intuitionist’s ¬A is effectively the modal □¬A.
Orjan:
Proving that there is no proof of A can be trivial; you just have to come up with a counterexample.
If A is “all numbers are even”, then saying “the number 1 isn’t even” is a proof that there is no proof of A.
With respect to the OR confusion: “v” always means inclusive or, as far as I’ve ever seen.
In intuitionism, “A v B” basically means “I know A or I know B, but I’m not telling you which”. To show that some other sentence C is a consequence of “A v B”, you have to show that C is a consequence of A alone (i.e., A→C) and that C is a consequence of B alone (B→C). This is also how you use a disjunction in classical logic.
I’ve never seen an “interesting” axiom system with a disjunction as one of its axioms, presumably because if you know that either A or B is true on intuitive grounds, you know which of them is true. There are things like the trichotomy law, but those are really universal generalizations over disjunctions, which are not the same thing.
Actually, there is just an axiom system. In synthetic differential geometry, they axiomitize the reals as both a totally ordered field and having nilpotent infinitesimals. Since you can derive a contradiction from these two facts in a second, they escape the contradiction by using intuitionistic logic.
I was having trouble reconciling this with the conventional wisdom that in intuitionistic mathematics “A or B” is true only if you have a proof of either A or B. The solution to the paradox is that while synthetic differential geometry uses intuitionistic logic, it’s not philosophically intuitionistic.
Intuistic logic really caught my attention. Although I probably really need to understand the logic part better, my interest lies more in numbers.
I am trying to define differentiation with the limit. (I have seen it defined in another way) I think i have succeeded, however, the limit has a problem.(That afaics just happens to not affect the differentiation.)
What i used is an axiom(and proofs they’re potentially true.) that infinitesimals g(x)=g(y). (one of)The latter functions is used to get an single value from the limit, which is otherwise defined as usual. The problem is that limit results are messed up by this. differentiable. Say f continuous as defined with a limit. Then it must be that with dx infi f(x+dx)=f(x), and thus the derivative is either not defined, or zero.
Other solutions to this don’t seem to work(Hmm, maybe try a function to fix it afterwards..), anyone know of someone trying to define things like this? I guess some kind of definition of limits is desirable regardless of whether differentation is defined in terms of it, such, is it not?
I wanted to link to my Decimal Godelization of a set of 11 axioms for Intuitionistic Logic, at the OEIS (Online Encyclopedia of Integer Sequences). But the OEIS is having one of their rare server problems. Hosted by AT&T Research Labs. Kind of an old-school equivalent of a gmail slowdown… So, can only suggest going to OEIS when it’s back up, and entering “Intuitionistic Logic” into its search engine. Comes with annotations, citations, links to related stuff.
http://www.research.att.com/~njas/sequences/A140861
I’m not retyping the propositional logic as 11 axioms here, because the implication arrows are drawn with “greater than” signs which the form parser thinks are parts of HTML expressions.
For a good background, see Mark van Atten, The Development of Intuitionistic Logic, Stanford Encyclopedia of Philosophy (available online), 10 July 2008.
Pingback: Programs As Proofs: Models and Types in the Lambda Calculus | Good Math, Bad Math