Lambda the Ultimate

A topic started by Hewitt, with the line "there seems to be a great deal of confusion and controversy on the part of both theoreticians and practitioners".

Stanford Encylopedia of Philosophy article on type theory; I've linked the section on set/type equivalence, an idea that goes back to 1908.

Just to name a couple recent efforts towards this, there is Homotopy Type Theory (HoTT) and Observational Type Theory (OTT).

Is there a list of type theories somewhere?

So I thought the same thing, but apparently HoTT is not intended to replace set theory, and some people are trying to prove HoTT consistent in set theory. Apparently the use of "foundational" is not what I first thought. This is not the impression I got watching Prof. Harper's video lectures on HoTT, so I was wondering how widespread the idea is?

HoTT as currently constituted has too many limitations to be a mathematical foundation for computer science.

Also, first-order set theory is inadequate.

but apparently HoTT is not intended to replace set theory

That's confusing. Do you have a link?

Some people do propose to replace set theory with (some variant of) HoTT. Replacing one foundation with another is a matter of opinion — tons of alternative foundations have been proposed, including type theory and category theory itself. I'm not sure why they do or don't succeed — mostly, people who care about foundations have trouble interesting other mathematicians, who typically don't care about foundational issues.

Moreover, HoTT contains things that behave like sets — it just contains other things in additions; so I'm not sure one can say that HoTT replaces set theory.

However, reading http://homotopytypetheory.org/ carefully reveals indeed a distinction between HoTT itself and Univalent Foundations, that is the plan for a new foundation of mathematics based on HoTT.

some people are trying to prove HoTT consistent in set theory

That's not necessarily evidence that one wants to keep set theory — there needs to be some proof that HoTT is consistent, and this proof should be relative to some known consistent theory. In fact, all mathematics is proven consistent relative to other consistent theories (like set theory); for some theories, however, doing that is inconvenient.

Didn't a formalization of HoTT introduce an inconsistency in Coq? I clearly remember something like that but the details are hazy. Something like the univalence axiom introducing equality on distinct small sets?

Anyone?

I might be wrong, but I don't think there are huge problems. It's likely some effort ran into issues that were fixed, but the whole HoTT book was first formalized in Coq and Agda (see e.g. https://github.com/HoTT/HoTT; I checked issues and I don't see any annoying inconsistency; "universe inconsistencies" are unrelated issues).

I'm sure somewhere somewhen somebody wrote inconsistent axioms, but that happens all the time — whenever you use axioms in theorem provers, you need to be very careful you're not introducing bugs.

In fact, univalence prevents introducing equality on distinct types, and that's known since when HoTT was invented.
Coq has an equality on distinct types, called heterogeneous equality. That's not used by default, but it's available. But it relies on an extra axiom, called axiom K, and that axiom is incompatible with univalence — so you can't use both together.
Agda had more problem, because it did use Axiom K by default for deep reasons; luckily an ICFP 2014 paper showed how to avoid that.

Sets should be constructed from types (which are more powerful), which is easy to do using type function spaces.

See
Derivation of Sets from Types

Keean,

Yes, it is possible to directly and intuitively construct mathematical sets from types using the following:
1) ℕ (type the natural numbers) axiomatized using the strong Peano/Dedekind axiomatization.
2) countable sums of types, i.e., ∐f where ∀[i:ℕ] f[i]:Type
3) characteristic functions, i.e., a set is defined by a function from a type into Boolean such that the elements of the set are exactly the ones where the characteristic function is true.

The above gives a unique model (by a unique isomorphism) of the sets of ordinary mathematics including the real numbers.

Please see the following article for details:
Inconsistency Robustness in Foundations

I thought they were two sides of the same coin, due to Curry-Howard. The types express the theory, and the program (lambda term) is the proof. This would imply that you cannot express theories in lambda calculus, nor can you express proofs in types?

Types are fundamental to both logical theorems and concurrent programs.

Curry-Howard doesn't do Jaśkowski Natural Deduction and it doesn't apply to concurrent programs.

The original purpose of the lambda calculus was to serve as the foundation of mathematics to express theories.

Why would I want to do Jaskowski natrual deduction? How do I express a theory in Lambda calculus and prove it?

Jaśkowski natural deduction is fundamental to mathematical proof. See the article referenced at the top of this article.

See the following for theories in the lambda calculus:
* Alonzo Church “A Set of postulates for the foundation of logic (1)” Annals of Mathematics. Vol. 33, 1932.
* Alonzo Church “A Set of postulates for the foundation of logic (2)” Annals of Mathematics. Vol. 34, 1933.

(I've been writing about this in a draft blog post, which is of course taking excessivley long to assemble.)

There's a folk interpretation of Curry-Howard as an anlogy between logic and computation. It's really, really not. The correspondence is between proofs and programs. Like this: modus ponens — which says that if A is provable, and A-implies-B is provable, then B is provable — corresponds through Curry-Howard to the typing rule for function application — which says that if you've got an expression of type A, and an expression of type function-from-A-to-B, you can syntactically combine them to form an expression of type B. A longer proof corresponds to a bigger syntactic program expression. Confusion arises because the two sides of the correspondence have very different purposes. The whole point of programming is the way the computation will evolve, which is described by the program syntax. The program syntax corresponds to a proof in logic. But the computation itself corresponds, on the logic side, to <drum roll> a sequence of proof transformations. Proof transformation isn't the be-all and end-all of logic; Curry-Howard is analogizing something of paramount importance on one side (evolving computation) to something that just isn't that big a deal on the other. Another way to put it is, the point of a proof is to elucidate why the conclusion is true, whereas the point of a program is to elucidate the algorithm by which computation evolves. You can't mazimize clarity of both of these at the same time; they pull in different directions.

I agree that reduction of lambda terms corresponds to proof transformation. The lambda terms still expresses a proof of a theorem though. Something like:

Prove: forall a . a -> a (prove there exists a function that maps all types to themselves)

is equally proved by either:

\x . x
(\z y . z y) (\x . x)

But only one is in normal form.

So if Curry-Howard is about the fact that reduction of lambda terms corresponds to proof-transformation, which theorem expresses the idea that the lambda term is a proof of some theory? Is it just a Godel number?

As proofs on the logic side correspond to terms on the program side, propositions on the logic side correspond to types on the program side. Demonstrating a proof of a theorem corresponds to demonstrating a term of a type. That is, a theorem is provable iff the corresponding type is realizable.

The following are legitimate types:
* ℕ axiomatized by the categorical Dedekind/Peano axioms
* ℝ automatized by the categorical Dedekind axioms

</i>

An Actor address must be typed in order to send it a message.

Consequently, a programming language must explicitly or implicitly supply a type in order to send a message.

However, there need not be anything "static" about the typing.

Constructive mathematics chooses infinity over law excluded middle.

You can often show (constructively) that excluded-middle-like results can be proved (not assumed) on finite objects, or more generally "discrete" object. For example if you have a decidable predicate P(x) on booleans {true, false}, then it is (constructively) true that either (exists b:bool. P(b)) or its negation holds. Maybe less obviously, for any two natural numbers n, m, then it is (constructively) true that either (n = m) or its negation hold (despite there being infinitely many natural numbers: they are discrete enough, hSet-like).

That why I'm saying that "the mother is infinity" ;)

With natural numbers and predicates you could construct turing machine interpreter and then comes diagonalization lemma where we construct a statement that is plain wrong and which negation is also wrong.

Even without the law of the excluded middle, paradoxes still exist. All you need to create a paradox is recursion (self reference) and negation. You can still get Girard's and Russel's paradoxes. You need some kind of stratification to prevent these.

The easiest example is the barber paradox, where the barber shaves all men who do not shave themselves. We then ask if the barber shaves himself. In Prolog:

shaves(barber, X) :- male(X), not shaves(X, X).
male(barber).

:-shaves(barber, barber).

This loops forever in Prolog. Datalog will reject the definition as unstratifiable.

Prolog is not an complete implementation of general predicate logic, so it could not be used as a reference point in the discussion.

In the case of barber paradox we just have both statements wrong "shaves(barber, barber)" and "not shaves(barber, barber)", so the statement "not shaves(barber, barber) or not not shaves(barber, barber)" is true and double negation could not be removed here.

The law of excluded middle is too optimistic. It states that at least one of two alternatives true. We now have both of them wrong.

Horn clauses do not need to be interpreted by Prolog. You can have sound unification (post unification cycle check) and a complete search strategy (iterative deepening), like I use in my implementation. It is sound and complete so can this be used a reference? (Although I actually think negation as a failure is a mistake, this problem persists with the inuitionistic logic definition of negation).

I don't get what you say about the barber paradox. We are told the barber shaves everyone who does not shave themselves. When we ask if the barber shaves himself, he does if he doesn't and he doesn't if he does (its just a reformulation of the Russell paradox). If you dismiss it so easily, I think you have not understood it.

The law of the excluded middle is not used here, the barber paradox holds in intuitionistic logic.

The core point paradox that you think that one of alternatives that you have specified must be true (A \/ ~A).

Intuitionistic logic is not so optimistic. It says that some alternative is false, or maybe both (~~A \/ ~A). Note that the stament ~~A = A does not holds in Intuitionistic logic.

Infinite cycle is quite in the line with Intuitionistic logic. It just says that you fail to prove both statement and its negation. No problem here, it is just two-way falure to prove (~~A /\ ~A).

Quoting from: http://www.mathedu.or.kr/source/Lecture/Set/Russell's_paradox.pdf

Theorem. The collection is contradictory even if the background logic is intuitionistic.
Proof. From the definition of R, we have that R∈R ↔ ¬(R∈R). Then R∈R → ¬(R∈R) (biconditional elimination). But also R∈R → R∈R (the law of identity), so R∈R → (R∈R ∧ ¬(R∈R)). But by the law of non-contradiction we know that ¬(R∈R ∧ ¬(R∈R)). By modus tollens we conclude ¬(R∈R).
But since R∈R ↔ ¬(R∈R), we also have that ¬(R∈R) → R∈R, and so we also conclude R∈R by modus ponens. Hence we have deduced both R∈R and its negation using only intuitionistically valid methods.
More simply, it is intuitionistically impossible for a proposition to be equivalent to its negation. Assume P ↔ ¬P. Then P → ¬P. Hence ¬P. Symmetrically, we can derive ¬¬P, using ¬P → P. So we have inferred both ¬P and its negation from our assumption, with no use of excluded middle.

The last statement means that both P and not P are unprovable. If you translate the statemet to prolog, this means that neither P nor ~P will ever complete with success.

The provided theorem contains an important error.

The law of excluded middle is sneaked into start of the it. It starts by implict deconstruction of the term (R∈R \/ ¬(R∈R)), but the term itself is never proved by it. So you cannot consider two alternatives before you prove at least one of them.

Basically, start proving assuming R∈R, but this assumption is on conditions of the theorem. It could be received from nothing only using the law of exlcuded middle.

Rather than looping forever you could detect they cycle in the proof, and terminate with not-proved. This would mean you would get not-proved from P and not-proved form ~P. Do you think that detecting these cycles, and concluding that it is not provable is sound?

Not proven, rather than not provable.

Loop detection is unsolvable in general (halting problem).

Its solvable in this case. If you arrive back at the same goal with no additional information then it is a loop. So considering the barber paradox, the clause head is (assuming all X's are male) :

1. shaves(barber, X) :- not shaves(X, X).

The proof search would be:

:- shaves(barber, barber).
1. shaves(barber, X = barber) :- not shaves(X = barber, X = barber).
1. shaves(barber, X = barber) <here we detect the cycle>

You might not be able to solve the general halting problem, but cycle detection seems to be useful for a common subset of problems.

For that purpose you need to add an addional inference rule just for this case. You could imporove you cycle detection paradox to include more and more cases, but you never will have an algoritm that solves all problems. This is impossible with modern definition of algorithm. Any such algorithm would either loop or there will be false positives or negatives.

For that particular case, using normal inferrence rules you could not prove neither "shaves(barber, barber)" nor "not shaves(barber, barber)". If you include oracle with loop detection, it would possibly solve this particular problem, but then it would likely fail to detect definition:

shaves(barber, X) :- not shaves(X, X, 0).
shaves(barber, X, i) :- not shaves(X, X, i+1).

If you would solve this case, I would be able to create another rule that would fail your loop detection algorithm.

he's not looking for ill-formed programs he's looking for proofs that depend on themselves.

If x can only be true if x is not true, then x isn't provable. That's something to look for.

If x can only be true if x is true then x is a tautology. That's something to look for.

You (sort of) have a point that it might be possible to hide a contradiction or a tautology with extraneous conditions that could be optimized out but won't be, but you haven't actually come up with an example of that. Your program doesn't have the same meaning as Russell's paradox.

You'd have to come up with something like that that you can prove has the same meaning as something detectable.

It would be interesting if you could come up with anything that can't halt that you can prove is meaningful. I suspect you can, but I don't have the expertise to do it.

Consider that a challenge. Come up with a meaningful query that can't be solved with a search that has detection of contradictions and tautologies.

I really look on this as an optimisation in an iterative-deepening search strategy. As such it doesn't really matter if you can escape it with an iterative variable. However this could be avoided with an induction rule. If we have proved for N, and we can prove N => N + 1 (which is in the rule itself) then it is proved for all N. Obviously you could complicate further by using reals and adding 0.5, although it would reduce to testing N in a sequence, this might be too costly.

While I've tried to tackle more advanced books before I realized that I should go back and familiarize myself with the basics so I'm reading the always entertaining Raymond Smullyan's "A Beginner's Guide to Mathematical Logic". I just read a nice little paradox setting me up for non-naive set theory:

Lets define Hypergame as the following:
a 2 player game where the first move by the first player is to pick a normal game to play (a normal game is one that can not have an infinite number of moves).
all of the rest of the moves in Hypergame are just playing that game that was chosen in the first move.

So is Hypergame a normal game? At first glance it seems it must be.
But if Hypergame is a normal game then the first move could be:
"lets play Hypergame"
then the second move could be "let's play Hypergame"
and the third move could be "let's play Hypergame"
...
So if Hypergame is a normal game, then it's not a normal game.

But if Hypergame isn't a normal game, then you can't play that line that makes it not normal, so if it's not a normal game then it is.
...

Back to loops in logic programs:
From a programmer's point of view x:- x (x is true if x is true) seems to make x multivalued, or to put it another way, it gives the solver permission to use narrowing on x over the value of truth. I have a little experience with the Curry programming language http://en.wikipedia.org/wiki/Curry_%28programming_language%29 which can use narrowing over some kinds of values and even structures to solve logic problems.

You might be interested in KiCS2 which can be switched between different search strategies. http://www-ps.informatik.uni-kiel.de/kics2/

So if you have
y :- x
and z :- ~x
then y is satisfiable
and z is satisfiable
but (y and z) can not be satifiable because they each depend on a different narrowed value for x.

Russell didn't define a properly typed set using {x|x∉x} which is equivalent to {x|true} because a classical set is never a member of itself.

But {x|true} is a pardoxical because {x|true}∈{x|true}

My understanding is that if you force a strict stratification, such that we append a "'" for each level above the ground. So a set of values has type Set, and a set of Sets has type Set'. In which case {x|x∉x} does not type check as x cannot be both a Set and a Set' at the same time.

The Principia (Russell and Whitehead) used stratification to prohibit impredicative definitions, that is, definitions that are are not strictly prior to what they define. The properties predicative and impredicative cannot be defined within the system, since they don't belong to any particular stratum.

Datalog finds a nice middle ground in that positive self references must be >= to the level, but negative must be >, so the set of all sets that are members of themselves would typecheck, but the Russell paradox would not.

The rule of Excluded Middle is OK even for the most powerful classical logic, but [Kao 2011] showed that it is not OK for inconsistency-robust logic .

More important than Excluded Middle is the rule of Proof by Contradiction, which is fundamentally important in both classical logic and inconsistency-robust logic but it is formalized differently:
* classical logic: rule applies to inference
* inconsistency-robust logic: rule applies to implication (which is much stronger than inference)

Excluded Middle, per se, doesn't have much to do with the resolving classical paradoxes, which is best accomplished using types.

Sorry, but theory of types is failed workaround.

First-order logic with arithmetics follows theory of types, but all paradoxes are still reproducable. This happens because we could encode higher level statements using arithmetics (for example pair of natural numbers k and l could be encoded as 2^k * 3^l, and everything else could be encoded using pairs and numbers if you get the drift (including Turing Machine and its interpreter).

Proof by Contradiction is just convinient istrument that could get you wrong. So radicals like me think that it has no place in math. We should just let it go and use it only for few niches where it actually works.

Math is about working with form of statements without considering the content. And to work will our form processing instruments should add as little errors as possible. The law of excluded middle adds errors to implication space of models complex enough and thus we could not rely on it.

By limiting self-reference to a strictly positive position, and being intuitionistic, Type Theory avoids those paradoxes. In other words these is no law of the excluded middle in Type Theory, nor do Girard's nor Russell's paradoxes hold.

You could encode self-reference using arithmetics and first order logic. Type theory does not catch this. Hint: turing machine, interpreter, and halting problem.

Types block "self-referential" sentences. For example, the Peano/Dedekind categorical induction axiom is as follows:

∀[P:Booleanℕ→  Inductive[P]⇨ ∀[i:ℕ]→ P[i] 
  where  ∀[P:Booleanℕ]→ Inductive[P] ⇔ P[0] ∧ ∀[i:ℕ]→ P[i]⇨P[i+1]

If types blocks natural number arithmetic and first-order logic then they are some other types then I know. Arithmetics, and basic induction, first order logic are all that needed to create turing machine interpreter. And with turing machine interpreter is possible to make self-referential statement (halting problem).

The property you are describing is the decidability of the type system. Type systems that are decidable always terminate, you cannot create a non-terminating type-expression in them.

The question is not about nominal types here. For nominal types you could have just one - natural numbers. However, if you have arithmentic, you could encode some program in a big natual number and then interpret it. And that program could have self-referential constructs, so it is possible to formulate a paradox with it if we have too optimistic Law of Excluded Middle, but on nominal level we will have just a set of predicates about numbers. Russel's type theory will see a single type naturals, thus would not notice self-referential constructs hidden in big number.

If a type system is decidable, you cannot make it fail to terminate. I don't understand your argument, it doesn't matter what encoding you express in the type system, you could not implement an interpreter for that 'big-number' that would fail to terminate.

Now the interesting question is what can you express (and not express) in a decidable type system.

Russel's theory of types was adverties not as solution to decideble type system (none cared about them at that moment), but as a way to prevent logical paradoxes. It does not help with it, as the real culprit of paradox is the law of excluded middle. The paradoxes just shift a bit further.

The usual classical view is that Godel style self-referential sentences lead to incompleteness results, not paradoxes. What paradoxes are you referring to stemming from LEM?

Let's f(n,k) universal function (that interprets function encoded with natural number n applying to argument k) and N is the code for the function F(k) = f(k,k)+1. With LEM we get (F(N)=f(N,N) \/ F(N)!=f(N,N)).

1. The first alternative is F(N)=f(N,N) => f(N,N) + 1 = f(N,N) => False
2. The second alternative is F(N)!=f(N,N) => F(N) != F(N) => False

So we get paradox with LEM and simple axioms of arithmentics (which are needed to build universal function). According to LEM one alternatives should be true, but both are false. The way out of it is dropping LEM (for example, by introducing notions of partial functions), and so there comes incompleteness result.

so there comes incompleteness result.

Right, so this universal function that enumerates all total functions in some set S (the computable functions, say) is not itself in S (edit: or rather F isn't). Why would we, upon learning this, discard LEM?

const never talked about totality. The problem is that he should have, though it takes a bit of attention to see. (Well, his reasoning is ambiguous and your objection might be the correct one, but I read it differently).

Take f(n, k) to be the standard universal function. Now, that's not a real function, but a partial function, and so is F; they can be undefined (because programs needn't terminate), and your reasoning doesn't apply then. What must happen is that f(N, N) is not defined, so F(N) is equally undefined but you don't get F(N) = f(N,N)+1 on naturals, so no problem.

If you instead replace f by an interpreter for a total language, you can redo the same reasoning, but that proves instead that F(k) has no code in this language, as Matt M mentioned.

This kind of matter is a bit tricky, but a good course on computability should clarify the matter.

Basically, LEM allows to throw any term on the table as a pair of mutually exclusive assumptions, and after that you need to fail just one of them, the other one will be automaticaly true.

With partial functions, you has to prove you right to have a term or its negation on the table at all. So LEM power is effectively reduced, it does not holds in general. You could not throw any equation on the table and start working with rewrite rules over terms. This is major shift of perspective. The question whether it is applied totally as in Intuitionistic logic or just locally (treating functions as some special objects).

The paradox stituation starts with LEM becuase LEM insists that exactly one of two terms is true statement, but it is not so with more complex statements. "Undecideble" is just another way to say that we cannot use LEM over it.

LEM sounds like negation as failure. I agree that not-proving a statement is not the same as proving the negated statement. If you cannot prove X is a member of Y, it does not mean you can prove X is not a member of Y.

The typical usage of LEM is proof via contradiction ~~A => A (which is LEM-equivalent), which is equivalent. We assume negative statement, receive contradication, and look, we have proved positive statement. We get barber paradox using it.

With partial functions, you has to prove you right to have a term or its negation on the table at all.

Right. We can keep LEM without paradoxes by only allowing it to apply to valid propositions. So regarding X = not X, we can deny that X is a valid proposition so that LEM doesn't apply to it. LEM is still valuable, though, because we can tell by looking at the form of many expressions that they are valid propositions.

(And thanks to Blaisorblade for correcting me. You were reading const correctly I think).

The whole point of LEM is that it is the axiom applicable to any proposition. If you need to prove whether LEM is applicable to the specific proposition, you would get some variant of Intuitionistic logic and no LEM in general, but LEM would be still applicable in some niches (like finite domains).

LEM is the statement "forall P, P\/~P". Anything less than it is not LEM but something else.

And you could not check the form of the expression to check if it is valid proposition (without false negatives or positives). At least you could not have algorithm that does it. See halting problem. You have to actually prove disjuction.

BTW Russel's failed attempt with Type Theory was attempt to allow only "valid" propositions basing on their syntax form. But type theory still allow arithmetic, and with that self referential statements using interpreters.

I don't understand where you're coming from. You seem to be making well understood points and then characterizing them in nonstandard ways. LEM appears in ZFC, probably the most widely used foundation of mathematics. If ZFC is known to be inconsistent, I've missed a development.

AFAIR ZFC cannot be proved consistent within ZFC, however it is not complete. ZFC puts a lot of defence layers to solve known paradoxes. Still it not known whether there are addional ones. And there are other approaches about it.

I have looked for refs, and I see that I was somewhat loosy with terminology here using "false" for "not true", due to viewpoint bias.

My understanding of incompleteness theorems that there are models and statements that neither statement nor its negation are provable in the model. If we equate true with being in theory of model (as in proof understanding of truth), as I have implicitly done then we get problem with the LEM. While it could hold from abstract truth value point of view, in constructive sense it might be unreachable within theory (there are no proof of it). When we deconstruct LEM(P) in constructive setting we kind of assume that we would have reached P or its negation if we have tried hard enough. Coq in some sense forces to actually to reach such statements before using it.

My point of view is that LEM in face of undecideable is at best a moot point and a potential jump out of the theory space. Russel's paradox happens because both propositions are outside of theory space and Russel has deconstructed term LEM(R contains R).

It seems like every type theorist these days is a philosopher of mathematics who finds LEM questionable. I don't get it. It seems obvious to me that e.g. the Collatz conjecture is either true or it isn't (even if turns out to be unprovable either way).

LEM has been suspected for about a century now. The better part of two centuries ago, the foundations of mathematics underwent a classic paradigm shift, so mathematics was then to be founded on axioms. The new axiomatic foundations of mathematics were hugely fruitful, but then around the end of the nineteenth century they discovered there were bugs in the system, antinomies provable using the axioms they'd settled on. Since they were getting a contradiction they figured they must have assumed something that wasn't true. And giving up a cherished axiom had worked really well for geometry, after all (opened up whole realms of non-Euclidean geometry). So they looked at this really pretty small set of axioms they had to work with, and tried to find one of them that didn't hold in general. LEM was, basically, the least absolutely solid axiom in their toolkit so they turned on it. (Not everybody turned on LEM; Hilbert figured it was just too useful to give up without a fight, and Church, following Hilbert's approach, considered maybe keeping LEM intact and instead weakening reductio ad absurdum. But that didn't work out either.)

That reads vaguely like history as I understand it, except that the version I know has the intuitionist camp (Brouwer, Heyting) as splitting from "everyone else" who kept LEM. I'm not a historian, but the fact that ZFC is the dominant system used today for axiomatic set theory makes me skeptical of your version of history.

I'm simplifying, of course. My point is that LEM was suspect; what individuals did about the suspicion would vary with the individuals.

the version I know has the intuitionist camp (Brouwer, Heyting) as splitting from "everyone else" who kept LEM

That sounds suspiciously like paranoia from the intuitionist camp. Or simply self-aggrandizement. As I recall, under Hilbert's program, where you used metamathematics to reason about a formal system, the rules of deduction he had in mind for the metamathematics were more-or-less intuitionistic (the term used was, iirc, finitary, or at least that's how it generally gets translated into English).

It still seems my understanding of history doesn't agree with your main point. Most mathematicians didn't (and to my knowledge still don't, growing numbers of type theorists notwithstanding) find LEM suspect. The paradoxes were resolved by removing impredicativity in various forms.

And programming practice is developing by adding self-references of some sort (functional programming, metadata, runtime codegen, reflection, recursion (including on types), feedback loops, etc).

I do recall any paradox that does not involve LEM or its equivalent at some point, so there is a reason to suspect it.

There's the Richard Paradox. And Curry's Paradox.

Both pardoxes are examples how sneaky LEM could be.

Richard Paradox assumes that such list could be built from the start. Without implicit LEM, how could you bring such list on the table? You would need provide algorithm that builds such list, and there is none.

The second paradox is the same. Some goal is assumed from nothing, but it is never constructed from premises (definition is not an assumption). It is just brought on the table form nothing. First you need to prove a right to bring it to table.

If we invoke Curry–Howard correspondence, then you starting assuming value of some type, but actually have never demonstrated that you could actually produce a value of such type using some other function.

On the Richard paradox, it seems as if you're conflating LEM with constructibility. On Curry's Paradox, I see nowhere in the reasoning by the formal system being shown inconsistent where something potentially nonconstructive is introduced; the meta-mathematical reasoning involved applies to any proposition one chooses to apply it to, but I don't find it credible that there are no propositions that can be expressed.

Let's separate to levels mathematics and philosophy in meta-math. On philosophy layer you could do anything including discussions if "all-mighty god is able to create rock he cannot destroy". I'm interested if these problems could be actually translated to formal logic. If paradox does not survive the translation, it is not so interesting. It is just loosy usage of the language.

On Richards, there is assumption out of the blue sky about existence of the list. The constructive way would be providing algorithm that creates such list. But there is a subtask of determining if statement actually defines a real number or not (Real(s) \/ ~Real(s)). There is even stronger than LEM principle (principle of bivalence) is assumed with respect of the predicate Real, as it is required to select number-defining statements from the set of all statements. There are also other problems, but for LEM, it looks like it is involved in its stronger incarnation.

Again, constructive logic does not prohibit propositions to be expressed. You just have it in the premises of the theorem, part of the model, or construct it from the above mentioned elements. You could even proof something from abstract premise, but you have justify you premise at some point.

Well, I've no disagreement with ascribing Richard to constructibility problems; I just don't tend to identify constructibility with LEM.

From Gödel's results, if an omniscient being were to provide information to a sufficiently powerful logic via an oracle, with the usual restriction that the oracle's answers are based solely on the questions asked of it, then the logic would either not be able to prove itself consistent, or would also be able to prove itself inconsistent. The logic, together with its interface to the oracle, translates the behavior of the oracle into claims about "truth", like a sort of I Ching. The resulting claims about truth necessarily have the property that either they don't include a claim that the logic is consistent, or they do include a claim that it is inconsistent. Whether that's an artifact of the translation, and there's some sort of non-propositional truth by which the omniscient being can be consistent and know it, is an interesting question; it might have a useful answer, in which case I'd be inclined not to treat it as philosophy.

LEM allows to cheat constructibility problem. Practically you have to use either LEM or its equivalent to avoid providing evidence. While making assumptions is fine, failing the assumption just says that assumption is wrong. It does not says anything about provability of other branch of disjunction.

I think that the current trend of working around problems that caused by LEM with banning impredicativity is fruitless. So far impredicativity was diagnozed as problem only when combined with LEM. If presented with choice, I would choose safe impredicativity in favor of LEM. The human language and software are increasingly self-referential, refletcting the fact that the world is completly self-referential (see system theory). We have to find ways to safely deal with it rather than inventing tricks to avoid this problem. Constructive approach looks like the way to go for now.

Also if we add LEM to Curry–Howard correspondence, we would suddently receive non-computable expression (while all others constructs are computable using strightforward rules). This alone should make it very suspicious. In Coq, LEM works as some functional parameter to other proof-functions, but it is not possible to implement such function and pass an actual value.

There are fairly reasonable computational interpretation of LEM in terms of interactive computations, where LEM is a callcc-using operation that captures the current context.

Specifically, if you are the user and I am the environment, and you ask me for a given formula A a proof of (A \/ (A -> False)), I will capture the current context of our interaction (let's name this context `k`), then provide you a mock function (A -> False) (that is, taking the "right" choice in the disjunction) that, if you ever invoke it with a concrete argument (t : A), restores the context k and instead makes the "left" choice in the disjunction with witness (t : A).

There are even clearer syntactic description in multi-succedent systems where the various formulas to the right of the sequent each correspond to a possible "output port" for the result of the communication -- the construction above uses call-cc as an arguably complex way to create an "output port" for A on the side, while continuing with a main computation of type (A -> False).

I find this a perfectly sensible computational behavior, but of course it gives weaker canonicity guarantees that the BHK-like witnesses of intuitionistic logic, where a closed value of type Nat is always a natural number. In this classical setting, what you get instead is a reified discussion that will require you to interact with it (possibly providing proofs or counter-proofs of stuff the opponent had no idea whether they were true or false) before eventually getting a concrete witness. Nothing is made up, but some things are left for you to do in the future.

For LEM in Coq, you need to procude term A \/ ~A. And there are two ways to produce it: provide A or provide ~A (it is computationally similar to haskell type Either).

The problem with provided iterpretation is that mock could never complete, so it is partial function A -> A\/~A at best. LEM is total function A -> A\/~A (because it is an axiom). So it does not gives full LEM. And I also somewhat skeptical of call-cc in general, IMHO it is quote loosy construct.

I don't think your counter-argument is sufficient. It is true that calling a captured continuation aborts the current computation, but it is not a form of partiality because there is no dynamic failure, the interaction continues correctly (only in a different computation thread, if you want). This requires care of course, but we have strong normalization results for systems with such features, for example:

• "A Notion of Classical Pure Type System", Gilles Barthe, John Hatcliff and Morten Heine Sørensen, 1993
• "Classical Fω, orthogonality and symmetric candidates", Stéphane Lengrand and Alexandre Miquel, 2008

(The former work handles dependent types, but it is formulated with a call-cc-like classical operator (it corresponds roughly to the first interpretation I proposed). This restricts evaluation strategies when compared to the abstract-machine representations of the second paper, which is more satisfying in that respect (it corresponds roughly to an indirect presentation of the second interpretation I proposed).)

I need to look at it and it would not be soon. But I'm kinda skeptical that the approaches would work with a generic predicate "completes(function_number, arugument)". To emulate LEM we need a total function.

I think that the current trend of working around problems that caused by LEM with banning impredicativity is fruitless.

I'm inclined to agree. Restricting things in order to ban paradoxes must restrict either too much or too little, per Gödel. I'm also skeptical of attempts to find a cheap loophole in Gödel's results, like an uncountably infinite alphabet or second-order logic. I do hope to get through the Gödelian knot, but I take those as examples of how not to do it.

Btw, the "current" trend of banning inpredicativity dates from about 1910. :-)

And it is is a pity that it is current for so long time :)

I think logic should be stressed to the boundary of its usability to get to next generation of the mathematics. The core activity of the mathematics shifted several times already: arithmetic, geometry and algebra, calculus, math logic and theory of algorithms. Each one was in some kind meta to the previous ones and each one was discovered as stable patterns over previous one (Platon would disagree, but it what humans are good for, seeing and abstracting patterns and meta-patterns). I think sooner or later we will see patterns of something new over the logic. Impredicativity fears just possibly delay such development.

Types mean that Gödel's "self-referential" sentences don't exist.

See the first article referenced in the post of this LtU topic.

"type List[T] = Nil | Cell(head : T, tail : List[T])" is a self-referential type statement. The fact could be dodged to some degree with fixpoint operator, but still essential syntax is self-referential (and fixpoint operator is a separate can of worms, as it restricts expressible types).

If we take mainstream technolgies like Java, there is plenty of self-referentiality in type system and VM level. Also java.lang.reflect and particularly java.lang.ClassLoader.defineClass() are also self-referential, and this was advanced further with java.lang.instrument API. Microsoft's .NET has similar technologies as well.

Recursive parameterized types do not allow "self-referential" propositions because "self-referential" propositions are constructed using fixed points that do not exist.

For example, the following is a recursive definition of Tree,

Discrimination Tree◅aType▻ between Leaf◅aType▻, Fork◅aType▻｡▮

Fork◅aType▻ ≡ [Tree◅aType▻, Tree◅aType▻]

If you split tree type definition in two statements instead of one, it means that two statements reference each others. So there is still self-reference in type definition, but with additional intermediate added. What is your point here?

Fixpoint is an attempt to severly restrict self-references. However fixpoint in classical form is able only to represent total functions and structures. Not all useful sturctures are total or could be proved as such. Web Server with dynamic content as whole is not a total function (but might have parts that could be described as total functions). The same problem with GUI applications. Web Servers and GUI apps are still intersting objects to consider. Considering external events, external mutable state (databases, message queues, and so on), and addition of the time would only make matter worse.

Java core library has about 200 classes starting with java.lang.Object that reference each other and cannot be easily disconnected. While some of that is just bad design (particularly in reflection and security area), there is still need to work with such knots in the way that is close to the language of the knot.

Fixed points do not exist with types. Consequently, instead of using fixed points, typed systems provide for mutually recursive parametrically typed definitions like the ones above.

The "self-referential proposition" that Gödel used in his results does not exist using types.

I guess Benjamin C. Pierce would not agree with you. He has used them in the "Types and Programming Languages" to describe recursive types.

Self-reference using intermediate is still a self-reference. It would be still a self reference even if you will use three intermediates.

Types are a framework in which fixed points don't exist.

It is very important to distinguish between the following:
* "self-reference" using fixed points
* recursion using types

Gödel famously thought that mathematics necessarily has the "self-referential" proposition I am not provable where the I comes from a fixed-point construction using an untyped notation for mathematics. Using typed recursion, it is impossible to construct such a "self-referential" proposition.

There seem to be no practical uses for such "self-referential" propostions in mathematics.

I guess we have some fudamental disagreemt on what are "types", "fixed point", or even "exist". I strogly suggest reading TAPL book before making such strong statements.

BTW java.lang.reflect is a quite practical package in Java. It is hard to write a big enough Java program without using it at all. Math that is unable to desribe such practical programs is not a practical math.

And there are plenty self-referential statements in mathematics. All induction statement are essentially self-referential. The same is for recursion. It is just choice whether to allow limited cases of self-referential statements or allow limited cases of LEM. If both are unrestricted, we get a problem.

Const,

Yes, we have some fundamental disagreements.

The TAPL book is in need of a serious update ;-)

Reflection in Java has fundamental abstraction and security issues :-(

However, strong mathematical induction can be used to provide a categorical axiomatization of mathematics as follows:

∀[P:Booleanℕ]→ Inductive[P]⇨ ∀[i:ℕ]→ P[i]=True
  where ∀[P:Booleanℕ]→ Inductive[P] ⇔ (P[0]=True ∧ ∀[i:]→ P[i]=True ⇨P[i+1]=True)

Note that the above is much stronger than what can be expressed in first-order logic.

Prof. Hewitt, for all I know you might well be a genius. But I don't think that excludes you from the academic process, and I can't presume you don't know it since you provided a formalization of it.

So, if you want to challenge standard point of views, you write a paper (which you did) and submit it to peer review like everybody else. And if reviewers reject it, you take the extra effort to make your argument clearer, until you get it published by making it convincing enough. Not sure that's modeled in your formalization, but that's a standard part of the practice of science.

I say this because I've spent lots of time reading several of your papers, and I've never found the clarity which I've come to expect from good papers. I don't seem to be alone there.
For instance, why's the self-consistency proof of mathematics not published in a peer-reviewed venue? Why doesn't your paper cite a peer-reviewed and published formalization of direct logic when it first mentions it? If there is no such thing, why aren't you writing it?

See book "Inconsistency Robustness" for published versions of articles.

Also, there are numerous online videos that have been published that cover the material in the book.

PS. I am sorry that you have had a difficult time reading my articles. I would be happy to answer any specific questions that you might have.

PPS. Academic politics in this area of research can be very complicated as explained in one of the articles in the book.

Personally, I've read the articles too long ago to remember detailed questions.

I'm interested about "published" in a venue that does serious peer-review. To pass peer review, you'd need to convince a third-party expert — by clarifying your argument. After all, thankfully, this is mathematics.

Anyway, I now see that people here on LtU have taken time to ask you patiently, in detail, clarifications, for instance on http://lambda-the-ultimate.org/node/4784?from=200&comments_per_page=200; and you've left most of them not fully convinced of some part of the argument. I won't try again.

In Computer Science, unpaid article reviewing is not adding much value to articles.

Articles are debugged mostly by colleagues (including students).

With respect to the discussion that your referenced, Matt M. said
That comment makes perfect [sense]

We've named people at the top of two out of three schools of thought (we're missing the logicists) who were clearly being wary about LEM. Most mathematicians just went about their business. What's the alternative? Stop using real numbers? I recall noting in my dissertation (but was more up on the details when I wrote it, of course) that Brouwer continued to contribute to areas of mathematics that weren't justified by his philosophy; doesn't seem surprising. Morris Kline, remember, who got a broader view of the grand sweep of mathematical history that most of us ever will (though we can get a taste of it by reading his magnum opus), observed that "Progress in mathematics almost demands a complete disregard of logical scruples."

I also suggested in my dissertation that the long-term fate of the three philosophical schools (logicism, intuitionism, formalism) depended not on their philosophical merits but on their technical profligacy. I suggested that Hilbert's formalism has been aphilosophically quite successful, because metamathematics is now a major element of the toolkit used by researchers regardless of their philosophy (wasn't Kleene, who wrote Introduction to Metamathematics, an intuitionist?). I'd add to that, that we've inherited a technical anti-paraodox strategy from the logicists (type theory), and the intuitionists have bequeathed to us skepticism about LEM.

By the time you get to the level of questioning LEM, you're deep into the quagmires of philosophy where there are people questioning all assumptions. It's obvious that there will reach a point where foundations cannot be justified so I don't see such philosophy as likely to be particularly fruitful. I'm interested in logics that don't have flaws as a practical matter. If we can prove a logic sound in ZFC, then, as a practical matter, it's free of paradoxes. LEM is intuitive and it works.

the intuitionists have bequeathed to us skepticism about LEM

Only in the same way that we've inherited "skepticism" of the parallel postulate. That is, we understand that there are models in which it doesn't hold that can be interesting to study in their own right.

Avoiding logical flaws is a very practical interest, I agree.

Only in the same way that we've inherited "skepticism" of the parallel postulate. That is, we understand that there are models in which it doesn't hold that can be interesting to study in their own right.

I don't think it's save to analogize the two in that way. We're all prettly clear that the parallel postulate doesn't hold for arbitrary geometries, and we're not inclined to assume we live in a world where it does apply. However, while it's certainly uncontroversial that there are imaginable logics in which LEM wouldn't hold, it's by no means settled that there isn't such a thing as absolute truth, and if there is such a thing, it's by no means settled that LEM doesn't hold for it. Indeed, when we talk about a logic not having flaws, it rather seems we judge what we mean by "flaw" against absolute truth.

The LEM is part of Boolean algebra, but not part of Heyting algebra. This is a consequence of negation and complement being the same operation in a Boolean algebra and different operations in a Heyting algebra. I think part of the problem is people tend to think a binary-state (true/false) == a Boolean, but it could also be a "Heytingean". It all depends on what you are talking about. Boolean algebra is the correct model for logic gates where "A or not A = 1" makes sense. Heyting algebra is the correct model for proofs, where "A (not proven)" is not the same thing as "(not A) proven". So there is nothing wrong with the LEM when used in the right context, it all depends on the type of thing you are modelling.

Matt, you're mostly right, but John Shutt is right as well, and what he's describing is also standard — it's the Hilbert program: http://plato.stanford.edu/entries/hilbert-program/

Hilbert bought LEM (and other debated concepts); but to convince others (including intuitionists), Hilbert wanted to show that LEM were safe to use (didn't lead to paradoxes) without assuming them, so proof theory was born. Proof theory only uses very "concrete" methods — nowadays, intuitionistic, syntactic methods, with total computable definitions — to show that a logic isn't contradictory. For comparison, you can think of modern syntactic proofs of type soundness. In fact, under Curry-Howard, to prove that a natural deduction system is consistent, you can just check that the corresponding type system includes an empty type, is sound and strongly normalizing. (In fact, the proof theory of many systems often needs extensions to fully finitistic methods, because of Gödel's result, but they try to limit these extensions).

Caveat: I never read a precise description of the relation between finitism, intuitionism and computability, maybe because finitism is not a precisely defined concept, but I've come to the same conclusion as John.

Yes, I think this was probably the sense in which John meant LEM was suspect and I have no argument with this account.

If ZFC were able to prove itself consistent, then we would know for certain that it isn't consistent. That's Gödel's Second Theorem: if a sufficiently powerful logic can prove itself consistent, then it is inconsistent. Turns out, "sufficiently powerful" is a lot less than complete. The formal system only needs to be able to prove true statements that say such-and-such machine on such-and-such input will halt; and be able to do some really pretty trivial deductions building on an already-available proof that such-and-such machine on such-and-such input will not halt. The "trick" is that if the formal system can prove iteself consistent, that's the already-available proof from which the formal system can then do a little simple deduction and prove itself to be inconsistent.

AFAIR ZFC cannot be proved consistent within ZFC, however it is not complete. ZFC puts a lot of defence layers to solve known paradoxes. Still it not known whether there are addional ones. [...]
I have looked for refs, and I see that I was somewhat loosy with terminology here using "false" for "not true", due to viewpoint bias.

Indeed, there are no known paradoxes in ZFC even though it includes LEM, and we have no "perfect" proof there cannot be paradoxes (there are in fact proofs, but they have stronger assumptions, so they are usually ignored for simplicity).

But as you say, non-constructive features like LEM create properties that constructivists don't like — in particular, even once you have proved something, you can't extract a witness (what you incorrectly call a proof). In particular, given a proof of ∃ x. P(x), we can only extract the x if the proof is constructive. Similarly, given a proof of A ∨ B, we can only know which between A and B was true if the proof is constructive. But nobody calls that a paradox. Generally, one should distinguish mathematical facts (LEM is not constructive) from resulting interpretations/opinions (LEM is bad).

Expressions such as "provable in the model" and "proof understanding of truth" suggest that you're confusing proof theory and model theory.

My understanding of incompleteness theorems that there are models and statements that neither statement nor its negation are provable in the model. If we equate true with being in theory of model (as in proof understanding of truth),

Incompleteness means that there are statements P such that P cannot be given a formal proof, and also not P cannot be given a formal proof. The whole definition is entirely proof-theoretic, and does not require model-theoretic concepts such as "model" or "truth".

While it could hold from abstract truth value point of view, in constructive sense it might be unreachable within theory (there are no proof of it).

As mentioned, you should say "there are no witnesses".

Outside of computability, essentially everything mathematics uses total functions on some well-known domain. So everything you will read assumes total functions without mention.

You could not throw any equation on the table and start working with rewrite rules over terms.

Well, those with partial functions aren't equations of the kind you consider. Or maybe I should say they aren't equations at all, and partial functions are not functions at all. When we have a partial function f and an argument x, but don't know whether f is defined on x, we can only write f(x) by overloading or abusing notation. I'd expect that, formally in logic, you should replace f(x) = y by Gives(f, x, y), where Gives is some predicate; for some f and x, there is no y such that Gives(f, x, y). (In fact, in set theory a partial function f could simply be a relation with some of the restrictions of a function).
Many of the usual manipulations work, but the one you did doesn't.

Hence, the issue is not that for some propositions we can't use LEM; the issue is that some "functions", namely partial functions, aren't really functions. Later you point out that it can be undecidable whether a function is defined for some input — and that's true. But you can never really talk about f(x) — that abuse of language is only valid if you prove that it's defined, and is valid because you translate it to "the y such that Gives(f, x, y)" (or something yet more formal).

If you're interested in incompleteness results (as opposed to paradoxes), I've recently been observing that proof of Gödel's First and Second Theorems (broadly interpreted) doesn't require LEM at all. As I've formulated it, the proof does require that a concrete proposition about the behavior of a Turing machine (machine T on input i halts with output o) cannot be both true and false; but it does not require that such a proposition be either true or false.

I do not mean to diminish the value of your remark: looking at the actual details of Gödel's theorem is not easy and can get technical. However, on an informal level the fact that LEM is not required is very clear. The proof of the first theorem builds an interpreter for the proofs of the logic inside peano arithmetic, and uses this interpreter to define a self-referential statement that cannot be proven.

The key to incompleteness is not any classical reasoning, but just a natural limit of consistent/terminating computational systems. The same technique is used to demonstrate that total languages cannot express (as a pure computation) their own evaluation function (it's less technical because for nice languages you can use proper datatypes instead of Gödel encodings), and that is a computational proof (of a negation) by essence.

There's a number of subtle points in the proofs which are in spirit classical — one can luckily avoid LEM, but they do require the double-negation translation. So, arguably, LEM can't be clearly unneeded.

For details, see Russell O'Connor's proof in Coq.

For starters, Peano arithmetic is classical logic.

Gödel builds an interpreter for classical logic inside a strongly normalizing system (classical logic itself). That seems to violate what we discussed about interpreters of strongly normalizing languages (they can't be expressed in the same language); however, this interpreter is not computational, it is just a predicate connecting inputs and outputs.

Finally, the proof (I forgot again where at the moment, but see Sec. 7 of the earlier link) uses a semantic of the object language in the metalanguage, so it either models LEM with LEM, or uses the double negation translation.

I didn't know about this presentation of a Coq proof, it is an excellent reference, thanks!

Agreed; Coq proof, good reference to have.

To be a bit clearer about what I've been up to. For the halting problem, it's really pretty easy to explain, at an elementary level, why the halting problem is uncomputable. It's long seemed to me Gödel's Theorems should be almost that easy to explain. Yet I've found the proofs esoteric; an elementary explanation glosses over things that seem really important (for example, "It turns out for a sufficiently powerful system you can always construct a statement that amounts to 'this statement cannot be proven'"), while the moment someone mentions Peano arithmetic I'd say it's no longer elementary. So I set out to prove the Theorems (in principle, rather than exact formulation) in a way that would be almost as elementary as that simple explanation of why the halting problem is uncomputable.

Part of what I've gotten out of the proof is a heightened appreciation of just how little actually has to be assumed to get the basic results. Gödel, so I understand, was concerned that his proof be very concrete (a valid concern at the time, I'd say); but my proof says pretty much nothing about how the formal system works (slightly more is needed for the Second Theorem, but even then the requirements aren't controversial things like LEM or reductio ad absurdum). I've got an odd, growing impression that the problem isn't really LEM or reductio ad absurdum, but something about the concept of negation itself. Which, once said, doesn't seem that surprising, at least once said at LtU, considering the discussions we've had here about negation.

Part of what I'm getting from this discussion is, my blog post doesn't need further embellishment; I really should get it out the door.

The halting problem proofs of [Church 1935] and [Turing 1936] provided the first valid proofs of the First Incompleteness Theorem because Gödel's results are invalid because of the use of "self-referential" propositions that do not exist. (In his article, Turing remarks that his work is very different from that of Gödel. Gödel admired Turing's work and thought that it was fundamental.)

I think the same thing, Negation is problematic. I think negation as failure is wrong for proofs. Consider predicate even:

even(z).
even(s(s(X))) :- exen(X).

odd(s(z)).
odd(s(s(X))) :- odd(X).

It should be obvious that "not even" is not the same as odd. The difference is clear if you ask what happens with "not even(X)."

This shows up in that a Boolean algebra complement and negation are the same thing, but in a Heyting algebra (which is the correct algebra for proofs) they are not.

I think that its because the "meaning" of not changes with what is negated. I currently think negation elimination is a possible answer. We limit ourselves to equality and disequality, and we solve negations by term rewriting. Something like:

even(X): X = z \/ X = s(s(X))

not even(X): -(X = z \/ X = s(s(X)))
-(X = z) /\ -(X = s(s(X)))
(X /= z) /\ (X /= s(s(X)))

And then solve by disunification. Now "not even" behaves exactly like odd.

What do you think of this approach?

I mentioned a logic language with narrowing above.

Maybe in a language that has narrowing saying:
odd(X) :- X ∈ ℕ, ~even(X)
works.

Natural(z)

Natural(S(X)):Natural(X).

Even(X): Natural(X), not Odd(X).

Yes, I think implicit in negation elimination is that you need to know the type of X. You might infer that X is a Nat from the definition of even, and then use that fact to derive not even. It might be easier if that type (or predicate in your example) were explicit.

The intention is you would still write the clauses in a Prolog style, the equalities are implicit in unification. The idea is that you eliminate the negation, and the disequalities, to end up back with clauses only involving unification after the term rewrite.

I had skipped the second half of what you wrote, but now that looks very interesting to me.

I have no idea how to solve
(X /= z) /\ (X /= s(s(X)))
it looks the same as what it started as to me.

How does one solve by disunification? I have no idea.

EDIT:
Note I am adding to this comment instead of posting a new one in order to be friendly to the "LTU breaks when there are too many posts" bug.

It occurs to me that you shouldn't complain that not even isn't odd.

If even is defined as (is an integer and has the property of being divisible by two) and odd is defined as (is an integer and the property of not being divisible by two) then anything that is not an integer is not odd, and anything that is not an integer is not even, but is not a member of the other set.

not odd(elephant) is true
even(elephant) is false

So expecting not odd to generate even is simply wrong. So your above example SHOULDN'T work. If you say it does, that's very confusing.

not odd(elephant) should be "false" or "not-proven" I think using false is a mistake. even(elephant) should also be not-proven.

For disunification see:
http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CL-jsc89.pdf

The solution to the above is:

not even: (X = s(z)) \/ (X = s(s(X)))

The Coq proof applies only to a restricted subset of first-order theories. It also makes use of an untyped syntax of sentences that allows "self-referential" sentences :-(

Type Theory is intuitionistic, so there is not law of the excluded middle (although it is admissible). So I don't see how what you state applies. In many type systems you cannot even define a function.

... yet the type system doesn't prevent the apparent paradox. There's in fact no paradox, but for other reasons (see subthread with Matt M).

I was thinking about the type-system itself. You cannot express the paradox in the type system itself. In dependent type systems there is no separate value level. Consider you take a non-dependent type system, and also have no separate value level. So the only objects are type level objects (which would be empty universes).

I was thinking about the type-system itself.

Ah, I see that you talk about that at least since http://lambda-the-ultimate.org/node/5136#comment-85140, but the rest of the discussion is mostly about a different topic: does imposing a type system prevent paradoxes at the value level? For some type systems, the answer is yes.

That's why Russell invented his type theory, after all. const's argument wasn't very clear, but he was talking about nontermination values and not nonterminating types. Additionally, type systems can prevent nontermination — most typed lambda-calculi are strongly normalizing (in their pure form), so they can't express nontermination or the universal function. You need to add a fixpoint construct to restore universality.

However, we haven't really fixed what we're talking about, and we don't seem to have a shared frame of reference, so it's hard to make precise statement.

You cannot express the paradox in the type system itself.

That's not very specific; I agree you don't get non-terminating type-level functions. A paradox is a proof of false, or (under Curry-Howard) a term with type \bot.

In dependent type systems there is no separate value level.

That's false. LF is a paradigmatic dependent type system and has clearly distinguished value, type and kind levels.

One related (but boring) true thing is that various calculi don't distinguish between terms and types purely by the abstract syntax, but only through the type system (though there's still a distinction). This is *common* in dependently typed languages, but not exclusive; and you still have a hierarchy of universes. This design choice is the defining characteristic of Pure Type Systems (PTS) (I'd recommend Hindley and Seldin's Lambda calculus book for a gentle intro), and essentially all typed lambda calculi you know can be modeled that way.

Another related and more interesting fact is that, once you move to a predicative system (a la Agda), some things that are values in System F must move one level up (to what's usually the level of types). That happens already in id id, where id is a polymorphic identity function; in Agda, to type this expression you must make id level-polymorphic, and the first id will be instantiated at a higher level. Therefore, the usual value/type/kind distinction doesn't work so well. (This ain't easy, so I've tried that out, see https://github.com/Blaisorblade/Agda/blob/40081ca861fef4aa9914fd4536d9c32f66727045/ImpredicativePolymorphism.agda#L59 if you care in detail).

Sorry, I guess I need to have said, dependent type systems need not have a separate value level. In that the dependent type system itself has a lambda. So all the values can be constructed from lambda's using church encodings, and lambda is part of the type system.

Unfortunately, this post was misplaced.

Please see the following topic:

Church's fundamental paradox:  "Is there such a thing as logic?" 

Having types means that there are no "self-referential" propositions. For example, the following procedure cannot be used to construct a “self-referential” proposition because having types means that fixed points do not exist:

NotProvable.[aPropostion:Proposition]:Proposition ≡  ⊬ aPropostion

An untyped version of NotProvable was used by Gödel to construct the following “self-referential” proposition: I am not provable.

Girard's paradox was invented in a typed system, precisely System U. The problem there is too much impredicativity; so types alone don't prevent Girard's paradox.

If you meant, for instance, Martin-Löf type theory, then I'd agree with you — because that's also predicative.

Girard's paradox makes use of a mythical universal type that doesn't exist.

I tend to agree with this, so I use a strict stratification and append a ' for each level above values so 1 2 3 would have type Int', and types Int' Float' would have type Numeric''. So all types would have type Type''.

What I have trouble with is explaining why this is better than datalog's approach, or the dependent typed approach of only allowing self reference in a strictly positive position.

What do you think?

What do you mean with "type that doesn't exist"? System U is a type system and types Girard paradox (see e.g. Lambda Calculi with Types, Barendregt, 1992). Are you redefining the concept of "type system" to exclude System U?

You can exclude System U by talking about strongly normalizing type systems. You could even claim that talking about non-strongly-normalizing type systems is pointless, and you might even have a point there. Is *that* your point?

Imagining that there is a universal type is a mistake. Unfortunately, System U incorporated this mistake and thereby allowed Girad's paradox.

I am not sure Girard's paradox requires a universal type. If we consider generic functions, then it is clear types can be arguments to functions like "f Int 3". Now what is the type of this function? 3 might easily have the type "Int", but what is the type of the type argument? Is it type? "f :: Type -> Int -> Bool"?

If f is of the following type:

[Type]↦([Integer]↦Boolean)

then the following is of type Boolean:

 (f.[Integer]).[3]

So if 'f' has the type "[Type] -> [Integer] -> Boolean", I am not sure what the square brackets mean?

In any case the type of the first parameter to 'f' appears to be [Type]? How does this avoid the paradox? The type of [Integer] appears to be [Type], what is the type of [Type]? What would the type of this function be:

((f.[Type]).[Integer]).[3]

Of course Type is of type Type :-)

If f is of the following type

[Type]↦([Integer]↦Boolean)

then f is a procedure that has one argument that is a type and the following is of type Boolean:

(f.[Type]).[3]

Since I'm not Hewitt, I might get this wrong in some ways. To save breath, I'm also not directly replying to every part of your post.

1. In your paper "classical inconsistency robust direct logic", you state that IRDL excludes proof by contradiction, so I find your statement that proof by contradiction is fundamental to mathematics and reasoning in general to be strange. Are you saying IRDL is not suitable for reasoning or mathematics because it excludes proof by contradiction?

Hewitt is recommending Inconsistency Robust Direct Logic for reasoning in systems where there may be a very large number of axioms that haven't been carefully verified to be consistent. In Inconsistency Robust Direct Logic, proof by contradiction is okay as long as it's under an implication, which ensures that you don't mistake your result for being unconditionally true.

This is different from the foundational systems for reasoning in mathematics and computer science, which use small numbers of axioms and are carefully scrutinized. For those, Hewitt recommends Classical Direct Logic (aka "Mathematics"). Since these systems must be consistent, proof by contradiction is permitted at the theorem level, rather than just under an implication.

So yes, Inconsistency Robust Direct Logic is not suitable for "Mathematics," but "Mathematics" is likewise unsuitable for large sets of axioms.

---

So I find your statement about "not not x" not being the same as "x" confusing, are you saying IRDL is also unsuitable for computing?

I think you might have misinterpreted this as referring to IRDL:

In intuitionistic logic, ¬¬¬Φ is equivalent to ¬Φ. However, intuitionistic logic is not very useful in computer science because ¬¬Φ is not equivalent to Φ :-(

I'm pretty sure what Hewitt means is "intuitionistic logic is not very useful [...] because [in intuitionistic logic,] ¬¬Φ is not equivalent to Φ."

It would seem that intuitionistic logic already inconsistency robust as you cannot use prove by contradiction.

I have not seen any proofs that you cannot construct the whole of mathematics in a constructivist way from intuitionistic logic, so I guess the idea that its not suited for mathematics, reasoning or computation is just an opinion?

Because the logic itself does not have double negation elimination as an axiom, it does not mean that it is not admissible. You can define double negation elimination in an intuitionistic logic. So for example I can define Boolean algebra in intuitionistic logic, so I fail to see how its use in computation is restricted.

Dependent type systems are intuitionistic, so doesn't intuitionistic logic relate directly to that which is computable?

I still don't really know Hewitt's work well enough to be sure, but consider this:

To say that something is suitable for "computation," one popular expectation is that it can support Turing-complete programming. Unfortunately, Turing completeness in constructive type theories tends to go hand-in-hand with unsoundness, in that every type has monstrous inhabitants that don't terminate. This casts doubt on constructive logic's usefulness for computation.

If you want to reason about whether a computation is a valid member of its type, you're dealing with a problem of unbounded nondeterminism: The computation must respond, but there's no bound on how soon it must respond.

Hewitt seems to be recommending a language, ActorScript, where he believes CSP's lack of unbounded determinism has been amended. He apparently finds it necessary to recommend Classical Direct Logic and Inconsistency Robust Direct Logic, so I bet these are how the type system of ActorScript has been formalized.

While your favorite approaches might lead to solutions as well, it's not enough to say that all the things in one mathematical foundation can be done in another. That's what makes them foundations! You'd have to argue why it's easier.

If you want to reason about whether a computation is a valid member of its type, you're dealing with a problem of unbounded nondeterminism: The computation must respond, but there's no bound on how soon it must respond.

If this is true for intuitionistic logic, then it must be true also for inconsistency robust direct logic.

You'd have to argue why it's easier.

From my perspective a foundation is better if it has less axioms. If intuitionistic logic can be a foundation for all mathematics and it has less axioms (no law-of-the-excluded-middle, no double-negation-elimination, no proof-by-contradiction) then it is clearly a better (simpler) foundation.

Foundations need appropriate, intuitive, strong axioms. Classical theories need all of the following:
* Proof by Contraction
* Double negation
* Excluded middle

I am not sure I agree with this. We can define axioms like the law-of-the-excluded-middle and double-negation-elimination inside intuitionistic logic, as they are admissible. You cannot do the opposite, un-define LeM in classical logic.

First-order set theory is inadequate for the foundations of Computer Science. For example, first-order set theory cannot even categorically axiomatize the natural numbers ℕ.

Intuitionistic logic can axiomatize finite natural numbers. Something like:

nat(z).
nat(s(X)) :- nat(X). 

You don't need infinite numbers for computation.

If you want to reason about whether a computation is a valid member of its type, you're dealing with a problem of unbounded nondeterminism: The computation must respond, but there's no bound on how soon it must respond.

If this is true for intuitionistic logic, then it must be true also for inconsistency robust direct logic.

Uh, yes? My goal with that paragraph is to describe a conundrum you might relate to, and which I suspect Hewitt has a particular way to deal with. If Hewitt really does, that doesn't mean the conundrum stops existing, but it becomes manageable.

Whether this conundrum is "true" doesn't exactly make sense to me. Since I'm talking about a reason to move from one foundation to another, I'm talking about a reason that is real enough that someone would care about it, rather than something that is necessarily a real problem from everyone's perspective.

From my perspective a foundation is better if it has less axioms. If intuitionistic logic can be a foundation for all mathematics and it has less axioms (no law-of-the-excluded-middle, no double-negation-elimination, no proof-by-contradiction) then it is clearly a better (simpler) foundation.

There are lots of reasons to choose a mathematical foundation, and sure, the raw number of characters in its implementation is one factor to consider. The conundrum I explained is another.

Keean,

Your axioms do not categorically axiomatize ℕ.

The Peano/Dedekind categorical induction axiom is as follows:

∀[P:Booleanℕ]→  Inductive[P]⇨ ∀[i:ℕ]→ P[i] 
  where  ∀[P:Booleanℕ]→ Inductive[P] ⇔ (P[0] ∧ ∀[i:ℕ]→ P[i]⇨P[i+1])

In computer science, categoricity is important to avoid nonstandard models.

Like most type theories, the above seems to presuppose the existence of integers, raising to a power, what a boolean is etc.

Can you start from something more primitive (and intuitive) and state the same axiom?

Why would I want a categorical introduction? Why is my axiomatisation not categorical? Given any object X I can prove whether it is a Nat or not by evaluating "nat(X)". So X can be said to be of type nat if "nat(X)" is true. That seems to be categorical to me. I can define addition over nats, as we need an operation for a complete category:

add(nat(X), nat(z), nat(X)).
add(nat(X), nat(s(Y)), nat(s(Z)) :- 
    add(nat(X), nat(Y), nat(Z).

Note this definition of add will only add correctly defined nats. So the definition of nat above and addition together form a category.

So the definition of nat above and addition together form a category.

"Categorical theory" (not to be confused with category theory) is a term from model theory. It means a theory that has only one model, up to isomorphism.

First-order theories of the natural numbers can always have models that include nonstandard numbers. In contrast, the second-order Peano axioms are categorical.

I'm repeating things I've heard, anyway.

How can any logic prevent you having nonstandard numbers? If my axioms permit 'i' as a number it is a number. Natural numbers are defined by an appeal to intuition nothing more.

By the Peano/Dedekind axioms, the natural numbers (ℕ) are characterized up to isomorphism via a unique isomorphism for which there is a proof in the following article:
Formalizing common sense reasoning

Consequently, there are no nonstandard natural numbers.

For example in the model I used above, natural numbers are modelled by object containment, so s(s(s(z))) is model of the natural number 3. Where is the model in your formulation above?

Up to isomorphism, the only model for the Peano/Dedekind axioms is the natural numbers N.

What is the structure of a natural number? Where does the definition of '+', Induction, Boolean come from. At the least what you have is an incomplete definition relying on assumptions that you don't explicitly state. Can you give the complete definition, or do you rely on a pre-defined meta-system with integers, booleans etc?

Keean,

The details can be found here:
Inconsistency Robustness in Foundations.

Okay, so I looked at that and I can see no definition of the set of natural numbers "ℕ", no definition of what a power is as in "Boolean^ℕ", no definition of the predicate "Inductive", and no definition of the operator "+".

For example in Prolog, I can define natural numbers with nothing except atoms, compound terms (objects which are syntactic in nature) and the concepts of inference, conjunction and disjunction.

How do I define what a "Boolean" is, and what "Boolean^ℕ" means?

Edit: I re-read the paper, and it still makes no sense to me. Things like "defining the turnstile symbol as mathematics". What on earth is mathematics? You seem to have introduced the whole of mathematics as a concept with no definition. You may as well say you have proved a horse consistent, as you could just as easily claim turnstile is a horse, dog or a cat.

Besides the idea that all mathematical systems are consistent is clearly wrong, consider the axiomatic system (using ~ for negation)

-------
 a true

-------
~a true

A logic that consists of a single inconsistent proposition.

Type theory of ActorScript is decidable in almost linear time, which is important for the performance of IDEs.

See Types in ActorScript

intuitionistic logic has proof by contradiction with the following rule:

(Φ⊢Ψ,¬Ψ)⊢¬Φ

Intutionistic Logic is *not* inconsistency robust because

Ψ,¬Ψ⊢¬Φ

I don't understand? given something and its negation you can infer something else? I don't recognise that axiom from intuitionistic logic.

It's not an axiom, it's a theorem, based on double-negation and reductio adabsurdum (if A implies falacy, then A is false). If you can prove two things that contradict each other, then you can assume the negation of any proposition A, derive a contradiction (because you could have derived that contradiction even if you hadn't assumed the negation of A), and conclude by reductio ad absurdum that the negation of A is false. Therefore, by double negation, A is true. No matter what A is.

That's why mathematicians were so upset around 1900 when they started turning up paradoxes in classical logic; and it's why a commonly used definition of an inconsistent logic is, a logic in which all possible propositions are provable. Wikipedia has an article, Principle of explosion.

Proof of inconsistency nonrobustness of intiutionistic logic:

(Φ⊢Ψ,¬Ψ)⊢¬Φ

Thus in intutionistic logic, the negation of every proposition can be proved from a contradiction.

Consequently, intutionistic logic is inconsistency nonrobust although strictly speaking it is not "explosive."

Apparently that does hold in an intuitionistic logic, but I don't understand why when double-negation elimination is not an axiom in intuitionistic logic.

However minimal logic is an inuitionistic logic that rejects the principle of explosion, maybe that's what I want.

I'm puzzling over that myself.

I was wrong about how false is defined, but intuitionistic logic comes with an elimination rule for _|_ that allows you to conclude any proposition from false. So the proof is:

Want: a -> (a -> false) -> b

Assume a and (a -> false). Apply modus ponens to conclude false. Use the elimination rule for false to conclude b.

In intuitionistic logic, false is defined to be forall a. a. So, if you can prove false, you can prove anything by definition. Negation is defined to mean implication of false, so a -> (a -> false) -> b is trivially proven by modus ponens (function application) followed by instantiation of false at b.

That definition is not regular intuitionistic logic, it is from System F or similar second-order logics.

I knew that. I was thinking of the calculus of constructions. Intuitionist logic does usually come with an elimination rule for absurdity, though, that lets you conclude whatever you want, doesn't it?

Yes, and you can bring the two close together by changing the elimination rule for bottom (which has no introduction rule) to be the axiom schema

    _|_
   _____
     P

which from the Hindley-Milner point of view has the conclusion P as being implicitly forall quantified. The HM-style implicit quantification is rather like System F, but where the forall quantifier can only be outermost: this has the consequence that the propositions for conjunction and disjunction can be defined in the System F way, but not the elimination rules which need a nested forall quantifier.

Bottom (⊥) is not a proper proposition because it does not say anything.

..because it doesn't count anything, is not a quantity, whatever.

This is monster barring, and it is a defect of an account that it fails to explain what other accounts do explain.

Of course, -1 denotes a proper number that can be used in numerical computations.

However, bottom (⊥) does not denote a proper proposition that says something.

Also, ⊥ makes no sense in Inconsistency Robust logic because the following are not equivalent:

    Ψ∧¬Ψ

    Φ∧¬Φ

(on pain of not being 'proper')

The number zero does not count anything, but we mostly do regard it as a proper number. Isn't zero to the counting numbers what absurdum is to propositions?

Telling someone False does not tell them anything :-(

Telling someone that their bank account balance is 0 says that there is nothing in the account.

False may have been OK in classical logic as an arbitrary inconsistent proposition because all inconsistent propositions are logically equivalent.
But it doesn't work in inconsistency robust logic.

..since the account might be overdrawn, or more accurate (e.g. due to interest paid to the nearest basis point) than the currency that can be drawn on them.

At this point, I'd like to refer you to chapter 3 of my doctoral dissertation [1], where I talk about the role that absurdum plays in argument, and the difference in meaning between it in classical and intuitionistic logic. For the tl;dr, the theory of argument may have a positive role for a empty propositions, so a theory of logic that rejects empty propositions is deficient from the point of view of such a theory of argument. That counts as a weakness with me.

[1]: On the formulae–as–types correspondence for classical logic. DPhil thesis, Programming Research Group, University of Oxford, 2000.

Thanks for the link to your thesis.
Unfortunately, it seems to be limited to first-order logic :-(
Please see Limitations of first-order logic.

The Peano/Dedekind induction axiom is categorical for ℕ because it quantifies over all uncountably many predicates of Boolean^ℕ as follows:

∀[P:Booleanℕ]→  Inductive[P]⇨ ∀[i:ℕ]→ P[i] 
  where  ∀[P:Booleanℕ]→ Inductive[P] ⇔ (P[0] ∧ ∀[i:ℕ]→ P[i]⇨P[i+1])

What is "Boolean^N" and where is it defined? Where are the elements of a boolean specified?

Superscripts are set theory notation for function spaces. X^Y is the set of functions from Y to X (because the cardinality of such a function space is |X|^|Y|). So Boolean^N presumably consists subsets of the naturals.

So how many functions in that space? There are 2 possible boolean values (not defined anywhere) and infinite Nat values. Does that represent all possible binary partitions of the natural numbers then?

So we are saying P is a function from Nat to Boolean, and it is inductive.

We then have:

(P 0) /\ (forall i . Nat i => P i -> P (i+1))

So we still have 'magic' symbols '0', '1' and '+' which I have no idea what they are supposed to do, and the type Nat does not seem to be defined anywhere.

Bool ^ Nat is the functions Nat -> Bool. You can think of this as representing a subset of natural numbers (it's a function that answers "is this number in the subset?").

Bool -> Nat is isomorphic to a pair of naturals (f True, f False), and that would be written Nat^Bool (or commonly Nat^2, since Bool is a 2 element set).

Induction states that if a subsets P of the natural numbers contains 0 and has the property that it contains n+1 whenever it contains n, then P is all of the naturals.

But where do the definitions of 0, 1 and + come from. How can you have a function from Nat -> Bool when you define neither?

Boolean^N is the type of all functions from N into Boolean.

Sets can be derivatively constructed from types :-)

Yes, I worked that bit out. I still don't get where '0', '1' and '+' come from though.

Beyond the induction axiom, the Peano/Dedekind categorical axiomatization of N has a few other axioms.

Can you post those other axioms / definitions on which your categorical axiomatization depends?

Peano/Dedekind categorical axioms are commonly found, but watch out for the limited first-order induction axiom in some presentations.

The remaining axioms can be found in the article on Classical Direct Logic.

I still can't find where you define the structure of 0, 1 or addition. Are you using Church encoding? What is the model for successor, is it object containment? I refer back to the prolog definition:

nat(z).
nat(s(X)) :- nat(X).

To me this is a fundamental definition because it simply declares two symbols 'z' and 's' to have the declared structure 's' can contain other 's' or 'z'. No definitions outside these two lined are needed except the understanding of structural nesting '(' ')', inference and variables. This defines the type of nat structurally (structural induction?).

I can't find an equivalent structural definition of natural numbers in your version. I really don't see any advantage of the categorical version. 'nat' is a formal proof that the object is a Nat, which seems as good as you could want. You pass nat an object, and if it is defined you have proved it is a natural number. The only improvement I can think of is to allow polymorphism over the structure labels, so you can prove an object has the structure of a Nat.

I still can't find where you define the structure of 0, 1 or addition.

The axioms for the natural number 0 and the Successor operation are on "Formalizing common sense reasoning..." page 100 (page 101 of the PDF). They're also on "Inconsistency Robustness in Foundations" page 50 (page 51 of the PDF).

Admittedly, I don't see either of those papers define 1 or +.

Of course, other Peano/Dedekind axioms (beyond the categorical induction axiom)
are as follows (quoted from the article that I linked above):

• 0:ℕ
• Successor:ℕℕ
• ∀[i:ℕ]→ Successor[i]≠0
• ∀[i,j:ℕ]→ Successor[i]=Successor[j] ⇨ i=j

The first axiom says nothing more than the equivalent axiom I posted:

nat(z).

The other axioms look wrong. Successor is a function from Nat to Nat, the successor of a nat "i" is not zero, and the successor of i is the same as the successor of j, if i and j are the same. Is there some axiom missing? For example:

successor(z) = a
successor(a) = b
successor(b) = a

Would satisfy those axioms.

That example doesn't satisfy the last axiom. Read about Peano axioms.

Edit: It's easy to come up with these yourself. You want zero to be a number, and the successor of any number to be a number. You want to require that successors of different numbers are different and not zero. Finally, you want that every number comes about through this process of starting from zero and applying successor. But that's tricky (try it). This what induction sort-of says - any property that holds for every step of this generation process holds for all natural numbers.

I don't see how those axioms (as I am ignoring any not in that post) lead to that result.

My suggestion satisfies the last axiom that says the successor of i is equal to the successor of j if i and j are equal.

Isnt there an axiom missing, something like:

forall i . i:Nat /\ successor[i]

Other presentations of peano arithmetic http://en.m.wikipedia.org/wiki/Peano_axioms seem reasonable to me. My comments have been more about the fundamental structure of repeated application of the successor function Successor^N(Zero) seemingly missing from the axioms presented so far in this discussion.

I can (and have read, although I don't know them by rote) read the Peano axioms. I can encode them in Prolog or Haskell, and did that in the HList paper. My comments are specifically about this presentation of the axioms. Part of the problem could be I am not sure how a function is defined in this syntax, and which arrow means what.

This is what I mean about it not being fundamental, if I need to know all this other stuff before I can understand it, the worse it is as a foundation. I dont think you really need anything beyond variables, atoms, conjunction, disjunction and inference. Every time you add something to this list you make the case for it being foundational significantly weaker.

You have the four original axioms (with a bit of imagination.) Now you can check for equality.

But you posted two equivalences as axioms instead of propositions.

successor(a) = b
successor(b) = a

Either these are two new axioms, and you introduced an inconsistency, or you meant it as a proposition:

exists a, b:Nat. successor(a) = b /\ successor(b) = a

Which could be proven false, probably given some induction scheme.

They were definitional equalities, but I admit I wasn't really sticking to the definition of axioms, but trying to suggest objects that could exist, and relations that did not appear to be disallowed by the axioms.

I take it that definitional equalities are introduced as axioms?

Please just explain to me how the four axioms written exactly as in the post above lead to the natural numbers.