The n-Category Café

Does anyone know yet if Fermat’s Last Theorem can be proved in EFA? I seem to remember early discussions where people were wondering if Wiles’ proof could be formalized in Peano arithmetic.

I’ve heard Angus MacIntyre talking about this. He is working on a paper arguing that Wiles’ proof translates into PA. I say ‘arguing’ rather than ‘proving’ because all he plans to do is show that the central objects and steps can be formalised in PA, rather than translate the entirety of Wiles’ proof, which would be a a ridiculously Herculean task. I don’t know if his paper is available yet, but there’s some discussion of it here.

So, I just spent a bit playing around with $I \Delta_0$ to get a sense for it. I wanted to build a Gödel coding, and I found I needed the following lemma (quantifiers range over positive integers):

$\forall_n \exists_N \forall_{k \leq n} \exists_{d} \quad k d=N$.

Easy enough in PA; it’s a simple induction on $n$. But in $I \Delta_0$ I can’t make that induction because there is no bound on $N$. (There’s also no bound on $d$, but I can fix that by changing the statement to $\exists_{d \leq N}$; this is also true and trivially implies the above.) I can’t fix it by adding in $N \leq n^{100}$ because that’s not true; the least such $N$ is of size $\approx e^n$. I can’t write $N \leq 4^n$ because I don’t have a symbol for exponentiation.

Anyone want to give me a tip as to how to prove this in $I \Delta_0$?

I have two naive questions:

On the wikipedia page “ordinal analysis”, RFA (rudimentary function arithmetic) is mentioned as having proof-theoretic ordinal omega^2, but nothing is said about it. Has anyone here heard of it? Is it EFA minus exponentiation?

Even if some systems may be too weak to be assigned proof-theoretic ordinals, is it possible to make sense of “if that system had a proof-theoretic ordinal in any reasonable sense, then this ordinal would be …”? In view of the wikipedia page on the Grzegorczyk hierarchy (which gives systems of strength omega^n), it is tempting to say that Presburger arithmetic “should” have strength omega.

What’s an interesting result about PRA?

It is suggested that PRA is an upper bound for what Hilbert considered to be finitistic reasoning.

Is there some other well-known way to rank them?

There are (e.g. by the class of their provably total functions), but I guess you want something similar to ordinal analysis. In that case check Arnold Beckmann’s project on dynamic ordinal analysis.

How interesting can they get before the hand of Gödel comes down and smashes them out of existence?

For most purposes the bounded arithmetic theory $V^0$ (which is quite similar to $I\Delta_0$) is the natural starting point. The provably total functions of $V^0$ are exactly $AC^0$ functions (the smallest complexity class complexity theorist usually consider). For comparison, provably total functions of $I\Delta_0$ are Linear Time Hierarchy (LTH). $V^0$ is capable of talking about sequences using a better encoding that Godel’s beta function (write the numbers in the sequence in binary, add 2 between each consecutive pair, read in base 4). It can also check if a given number encodes the computation of a given Turing machine on a given input.

But a more natural theory to work with might be $VTC^0$ whose provably total functions are complexity class $TC^0$ which can also parse syntax. See Cook and Nguyen (draft) for more information.

I think self-verifying theories that can prove their own consistency (in the usual formalization) are artificial. For more information about them see:

Dan Willard, “Self Verifying Axiom Systems, the Incompleteness Theorem and the Tangibility Reflection Princible” , Journal of Symbolic Logic 66 (2001) pp. 536-596.

Dan Willard, “An Exploration of the Partial Respects in which an Axiom System Recognizing Solely Addition as a Total Function Can Verify Its Own Consistency”, Journal of Symbolic Logic 70 (2005) pp. 1171-1209.

I just spent a bit playing around with $I\Delta_0$ to get a sense for it. I wanted to build a Gödel coding …

You cannot prove that in $I\Delta_0$ because that would give a exponentially growing function while $I\Delta_0$ is a polynomially bounded theory.

On the wikipedia page “ordinal analysis”, RFA (rudimentary function arithmetic) is mentioned as having proof-theoretic ordinal $\omega^2$, but nothing is said about it.

Rudimentary sets are defined in Smullyan 1961. They are essentially $\Delta_0 = LTH$. I am not sure about the theory RFA but I would guess it is essentially $I\Delta_0$. EFA is $I\Delta_0 + EXP$ (where $EXP$ expresses that the exponential function is total).

Even if some systems may be too weak to be assigned proof-theoretic ordinals …

See above (the part about Beckmann’s research).

Thanks for posting this, John.

(Small quibble though - you have “$Q$ only has inductive definitions of addition, multiplication and exponentiation”, but $Q$ lacks the primitive recursive defn for exponentiation. Those axioms would be:

$(E_1)$: $\forall x(x^0 = S(0))$

$(E_2)$: $\forall x \forall y(x^{S(y)} = x \times x^y)$

But in standard logic, simply assuming a function symbol more or less presupposes the totality of corresponding function, i.e., exponentiation in this case. I.e., if we have a primitive binary symbol (i.e., $x^y$), then $\forall x \forall y \exists z (z = x^y)$ is a theorem of logic! For if $f$ is, say, a 1-place function symbol, then $\vdash \forall x(f(x) = f(x))$. And this gives us $\vdash \forall x \exists y(y = f(x))$. Quick indirect proof: suppose $\exists x \forall y(y \neq f(x))$. So, $\forall y(y \neq f(c))$, by introducing a new constant $c$; which gives the contradiction $f(c) \neq f(c)$.)

When Joel David Hamkins says that any weak system in the hierarchy $I\Sigma_n$ simulates computation, I think (I am guessing) he just means that any recursive function is representable in $Q$ and its extensions. E.g., if $f : \mathbb{N}^p \rightarrow \mathbb{N}$ is a partial recursive function, then there is an $L_A$-formula $\phi(y,x_1, \dots, x_p)$ such that, for all $k, n_1, \dots, n_p \in \mathbb{N}$,

if $k = f(n_1, \dots, n_p)$, then $Q \vdash \forall y(y = \underline{k} \leftrightarrow \phi(y, \underline{n_1}, \dots, \underline{n_p}))$

In particular, exponentiation, $f(a,b) = a^{b}$, is recursive. So, there is an $L_A$-formula $\mathbf{Exp}(y, x_1, x_2)$ such that, for all $n, m, k \in \mathbb{N}$,

if $k = n^m$, then $Q \vdash \forall y(y = \underline{k} \leftrightarrow \mathbf{Exp}(y, \underline{n}, \underline{m}))$

So, $\mathbf{Exp}(y, x_1, x_2)$ represents exponentiation. However, $Q$ cannot prove it total. I.e., for any such representing formula $\mathbf{Exp}$,

$Q \nvdash \forall x_1 \forall x_2 \exists y \mathbf{Exp}(y, x_1, x_2)$

It’s a long time since I worked through some of the details of bounded arithmetic, and my copy of Hayek and Pudlack is in Munich. So I can’t see immediately how to give a model for this. Still, $Q$ is very, very weak and here is a simple non-standard model $\mathcal{A}$. (From Boolos and Jeffrey’s textbook.) Let $A = dom(\mathcal{A}) = \omega \cup \{a, b\}$, where $a$ and $b$ are new objects not in $\omega$. These will behave like “infinite numbers”. We need to define functions $S^{\mathcal{A}}, +^{\mathcal{A}}$ and $\times^{\mathcal{A}}$ on $A$ interpreting the $L_A$-symbols $S$, $+$ and $\times$. Let $S^{\mathcal{A}}$ have its standard values on $n \in \omega$ (i.e., $S^{\mathcal{A}}(2) = 3$, etc.), but let $S^{\mathcal{A}}(a) = a$ and $S^{\mathcal{A}}(b) = b$. Similarly, $+$ and $\times$ are interpreted standardly on $\omega$, but one can define an odd multiplication table for the values of $a +^{\mathcal{A}} a$, $a +^{\mathcal{A}} b$, $a \times^{\mathcal{A}} b$, etc. Then one proves $\mathcal{A} \models Q$, even though $\mathcal{A} \ncong \mathbb{N}$. This model $\mathcal{A}$ is such that,

(i) $\mathcal{A} \nvDash \forall x \forall y(x + y = y + x)$

(ii) $\mathcal{A} \nvDash \forall x \forall y(x \times y = y \times x)$

So, this tells us that $Q$ doesn’t prove that $+$ and $\times$ are commutative.

I don’t think this simple model $\mathcal{A}$ with two infinite elements, $a$ and $b$, is enough to show that $Q$ doesn’t prove that exponentiation is total.

The idea would be to find a model $\mathcal{B} \vDash Q$ such that $\mathcal{B} \nvDash \forall x_1 \forall x_2 \exists y \phi(y, x_1, x_2)$, for any $L_A$-formula $\phi(y, x_1, x_2)$ that represents $f(a,b) = a^b$ in $Q$. I don’t know off-hand what such a model $\mathcal{B}$ looks like though.

Jeff

On one of Kaveh’s points, another property of PRA is that if $\phi$ is a $\Pi_1$-sentence, then:

$I \Sigma_1 \vdash \phi$ iff PRA $\vdash \phi$. (Parsons 1970)

Yes, Tait has argued that PRA represents the upper limit on what a finitist should “accept”. However, I think that Kreisel had argued earlier that it should be PA.

Jeff

Here’s another system (call it FPA) which proves its own consistency. Work in 2-nd order logic, with predicative comprehension. Let 0 be a constant; let N be a (1-ary) predicate, meant to represent being a natural number; and let S be a (2-ary) relationship, meant to represent the successor relationship. Do *not* assume the totality of S. Instead assume

(1) S is functional, i.e. Nx and Sx,y and Sx,z implies y = z
(2) S is one-to-one, i.e. Nx and Ny and Sx,z and Sy,z implies x = y
(3) (for all n) not Sn,0
(4) Induction (full induction, as a schema)

Because the totality of S is not assumed, FPA has the singleton model {0}. It also has all the initial segments as models, as well as the standard model (well, whichever of those models actually exist). In a nutshell, FPA is “downward”; if you assume that a number n exists, then all numbers less than n exist and behave as you expect. Most of arithmetic is, in fact, “downward,” so FPA can prove most familiar propositions, or at least versions of them. It can prove (unlike Q) the commutative laws of addition and multiplication. It can prove Quadratic Reciprocity. It cannot prove that there are an infinite number of primes (it cannot even prove the existence of 2, after all), but it can prove that between n/2 and n for any n > 2, there always exists a prime. It’s not far-fetched to think that FPA can prove Fermat’s Last Theorem. So, mathematically anyway, it’s pretty strong. (Still it’s neither stronger nor weaker than Q. It’s incomparable, because it assumes induction, which Q does not, but does not assume the totality of successoring, which Q does.)

In particular FPA can talk about syntax because syntactical elements can be defined in a downward way. Something is a term if it can be decomposed in a particular way. Something is a wff if it can be decomposed in a particular way. Etc.

Now, to prove its own consistency, it suffices for FPA to show that the assumption of a proof in FPA of “not 0 = 0” leads to a contradiction. But a proof is a number (in Godel’s manner of representing syntactical elements) and, in fact, a very large number. This large number then gives enough room, in FPA, to formalize truth-in-the-singleton-model and to prove that any sentence in the inconsistency proof must be true. But “not 0 = 0” isn’t true. Contradiction! Therefore FPA has proven its own consistency.

Here’s a link to a book-long treatise, if it interests anyone:

• Andrew Boucher, Arithmetic Without the Successor Axiom.

Thanks for your comment. Unfortunately, I don’t think it’s quite right and F does indeed interpret syntax adequately, so that it does express notions of consistency.

First, just as F is agnostic about the infinity of the natural numbers, it is agnostic about the infinity of the syntax. The infinity of syntax comes from assuming that there are an infinite number of variables; F doesn’t make this assumption. I guess a stickler might say this is no longer second- (or first-) order logic because these assume that there are an infinite number of variable symbols. But I would hope most would agree this is not an essential feature of the logic.

JK: “Incidentally, this already goes beyond F itself, as the metatheory already implicitly assumes the distinctness of these numbers. How would this be done, given that one cannot even prove the existence of 1?”

While one cannot prove that 1 exists, it is possible to prove that anything which *is* one is unique (and so distinct). That is, it is possible to define a predicate one(x) as (Nx and S0,x). It is not possible to prove that there exists x s.t. one(x), but it *is* possible to prove that (x)(y)(one(x) and one(y) implies x=y). So proof of existence, no; proof of distinctness, yes. One can define two(x) as (Nx and there exists y such that one(y) and Sy,x). And so forth as far as one wants or has energy to go.

Moreover, one can define the concepts of odd and even. One defines even(x) iff Nx and (there exists y)(y+y = x). Again, no assertion that one can prove that even(x) or odd(x) for any x. But one *can* prove that there is no x such that both even(x) and odd(x). Again, existence no, distinctness yes.

So one can represent the syntax. Define predicates one, two, three, … , ten. Define Big(x) as Nx and not one(x) and not two(x) and … and not ten(x). Then x represents a left parentheses if x = 0. x represents a right parenthesis if one(x). x represents the implication sign if two(x). x represents the negation sign if three(x). x represent the equal sign if four(x). And so forth. x represents a small-letter variable if Big(x) and even(x). x represents a big-letter variable if Big(x) and odd(x).

One gives the usual recursive definitions to syntactical entities like AtomicWff(x) and Proof(x). Again, one cannot show there exist any x such that AtomicWff(x). But one can show that, *if* AtomicWff(x), then x has all the properties that it should have.

So, given that x cannot prove there exist any syntactical entities, how can it prove its own consistency? Because consistency means there is no proof of “not 0 = 0”. So a proof of consistency is not a proof that something exists, but a proof that something does not exist. It *assumes* the existence of a syntactical entity, in this case a proof of “not 0 = 0”, and shows that the assumption of the existence of this entity leads to a contradiction. Thus F is able to prove a system’s consistency. (What F cannot prove is prove that a system is inconsistent; because then it would have to prove that there exists something, namely a proof of “not 0 = 0”, and that it cannot do.)

Anyway, all this is described in gory detail in the link that I gave.

t, “One gives the usual recursive definitions to syntactical entities like AtomicWff(x) and Proof(x).”

What, exactly, are these entities $AtomicWff(x)$ and $Proof(x)$? How many symbols do they contain? Are they distinct? How does one prove this? Have you ever tried to estimate how many symbols occur in the arithmetic translation of the sentence

“the formula $\forall x(x = x)$ is the concatenation of $\forall x$ with $(x = x)$”?

You’re assuming something that you then claim to “doubt”. You do not, in fact, “doubt” it: you assume it.

One never says, in discussing the syntax of a language, “if the symbol $\forall$ is distinct from the symbol $\mathbf{v}$ …”. Rather, one says, categorically, “the symbol $\forall$ is distinct from the symbol $\mathbf{v}$”. The claim under discussion amounts to the view that one ought to be “agnostic” about the distinctness of, for example, the strings $\forall x(x = 0)$ and $\forall y(y \neq 0)$.

One can write down a formal system of arithmetic which has a “top” - called “arithmetic with a top”. But it is not as extreme as $F$. Such theories have been studied in detail by those working in computational complexity and bounded arithmetic (see, e.g., the standard monograph by Hajek and Pudlak, which I don’t have with me). See, e.g., this:

http://www.math.cas.cz/~thapen/nthesis.ps

Agnosticism about numbers = agnosticism about syntax. You can’t have your “strict finitist” cake, while eating your syntactic cake, as they’re the same cake!

Jeff

Sorry, it’s the end of the week-end, so this is the end of the road for my comments in this thread. If you’re interested, have a look at the link I put in my first comment. Thanks and bye.

I’m trying to understand this discussion. It seems to me that Jeffrey Ketland is saying, roughly, that because our usual theory of syntax can prove that the system $F$ has infinitely many formulas, while $F$ has finite models (as well as infinite ones), the system $F$ is ‘incoherent’ as a theory of arithmetic. For example, he says:

To repeat: form the point of view of ontology, interpretability, etc., syntax = arithmetic. The same thing. They can be modelled in each other. To “doubt” arithmetic while accepting syntax is incoherent.

So the language $L_F$ itself is countably infinite. Denying the existence of numbers while asserting the existence of infinitely many syntactical entities is incoherent, as one of Gödel’s basic insights is: syntax = arithmetic.

But this is puzzling in two ways. First of all, I don’t think $F$ “denies the existence of numbers”: any model of Peano arithmetic will be a model of $F$, so you can have all the natural numbers you might want. There’s a difference between denying something and not asserting something.

But more importantly, I don’t really care whether $F$ is “incoherent” from the point of view of “ontology” due to some claimed mismatch between the syntax of theory $F$ (which has infinitely many formulas, according to standard mathematics) and the models $F$ has (which include finite ones). “Incoherent” and “ontology” are philosophical notions, but I’m a mere mathematician. So I’m much more interested in actual theorems about $F$.

If these theorems are proved in a metatheory that can prove $F$ has infinitely many formulas, that’s fine! — just make sure to tell me what metatheory is being used. And if someone has proved some other theorems, in a metatheory that can’t prove $F$ has infinitely formulas — in other words, a metatheory that more closely resembles $F$ itself — that’s fine too! All I really want to know is what’s been proved, in what framework.

But I guess it all gets a bit tricky around Gödel’s 2nd incompleteness theorem. What does it mean for $F$ to “prove its own consistency”? I guess it means something like this. (I haven’t thought about this very much, so bear with me.) Using some chosen metatheory, you can prove

$$F \vdash Con(F)$$

where $Con(F)$ is some statement in $F$ that according to the chosen metatheory states the consistency of $F$. The Hilbert-Bernays provability conditions are supposed to help us know what “states the consistency of $F$” means, but if you want to use some other conditions, that’s okay — as long as you tell me what they are. I can then make up my mind how happy I am.

Here is a question that might be of interest to people here: are there any applications of restrained logical systems to ordinary mathematics? [NB What I wrote below grew a bit long. I hope it’s still OK to post here.]

Let me explain what appears to me to be a similar situation in algebraic geometry. (I know essentially zero about logic, so there’s a chance this parallel is completely ill conceived.) Usual, complex algebraic geometry is about studying complex solutions to systems of polynomial equations. Arithmetic algebraic geometry is about studying solutions in rings of arithmetic interest, most importantly the integers, but rings of derived interest are also important, like the rationals, finite fields, p-adics, etc. An important first step in finding arithmetic solutions to a polynomial system is understanding the nature of its complex solutions. When you have one polynomial in one variable, arithmetic algebraic geometry is really just classical algebraic number theory, and the same principle applies there — it’s just so simple you don’t notice it. This is because the qualitative behavior of the complex roots of a polynomial pretty much only depends on its degree. (I say pretty much because things are a bit subtler if you have multiple roots, but this is a degenerate case.) But as any student of Galois theory will tell you, if you want to study the roots of a polynomial, the first thing you need to know is its degree.

The parallel I’d like to draw, then, is between logical systems and algebraic geometry. Formal logic involves syntactic reasoning according to some rules, just like working in an algebraic structure, such as a commutative ring, does. Since algebraic geometry is pretty much just the study of commutative algebras slightly dressed up, I hope this analogy is reasonable. In this analogy, arithmetic algebraic geometry could be viewed as a restrained form of complex algebraic geometry because all the theorems have to be about systems of polynomial equations with integer (say) coefficients rather than complex ones. Similarly a retrained logic can’t use all the axioms of usual logic.

Now many mathematicians’ reactions to arithmetic algebraic geometry would be to say “Don’t tie my hands! I have no particular interest in number theory. I want to look at all solutions. I don’t really care about the ones that happen to be integral.” Similarly most mathematicians have no particular interest in restrained logics, even if they grant that they are valid mathematical objects. They just want to use logic, and so they want as much freedom with it as possible. So they add the axiom of choice, universes, etc.

This is a perfectly reasonable approach most of the time, but there are some exceptions on algebraic geometry side of the analogy, and what I’m wondering is whether there could be similar exceptions on the logic side. But there are really two kinds of exceptions, and I should say something about both.

The first is that sometimes in the world of complex algebraic geometry, structures of an arithmetic nature come up. A parallel in the logical world is that sheaves conform to a restrained logic. So even if you started out not caring about non-classical logics, you might decide it’s more efficient for you in your study of sheaves if you know something about restrained logics. The example I’m thinking of in algebraic geometry is in the study of abelian varieties. The endomorphism ring of an abelian variety is a ring which is finitely generated as an abelian group. Therefore it has an arithmetic nature, and knowing something about this will help in your study of abelian varieties. Such examples are only so interesting, I think, because even though the original objects of study did not have a restrained nature, there’s no reason to expect that objects derived from them would also not have such a nature. Even so, I’d be interested in knowing more examples in logic.

The second kind of exception is what I really want to talk about. Let me give an example in algebraic geometry. Suppose you want to study the complex solution set of a system of polynomials. If that system has integer coefficients, then you might be able to reduce everything modulo a prime, make some deductions about the solutions modulo that prime, and then draw some conclusions about the original system. For instance if you’re studying solutions to $x^n=1$, then you just have roots of unity, and I hope it’s plausible that some facts about complex roots of unity could be proved by working modulo primes. (This is in fact true.) But let me consider this from the point of view of the rings that come up in such arguments. The relevant ring if you’re studying complex solutions to $x^n=1$ is $C[x]/(x^n-1)$. If you’re studying arithmetic solutions, you want to look at the subring $Z[x]/(x^n-1)$. The subring has fewer elements. How could it be the case that confining ourselves to it is helpful? The reason is that precisely because there are fewer elements $Z[x]/(x^n-1)$, there are *more* maps out of it. In particular, you have maps to finite fields, rings which a complex die hard might consider exotic and non-classical.

So my first question is whether such a thing ever happens with restrained logics. Do restrained logics admit more specializations to other logics (in some sense), and could it happen that this is useful in studying classical logics?

I could stop here, but in fact the story continues. A complex die hard might say “OK, I concede that if the original polynomial equations have an arithmetic nature, then it can happen that things I care about can be proved using arithmetic. But this is exceptional. Indeed they form only countably many examples in a sea of uncountably many polynomial systems with complex coefficients.” This is a reasonable point of view, and I’d say that you have no right to expect otherwise. But amazingly sometimes arithmetic methods can still be used to do things when the original equations have arbitrary coefficients. The technique I have in mind is called “spreading”. Let $R$ be the subring of the complex numbers generated by all the coefficients in the system of polynomial equations. If one of the coefficients is transcendental, like $\pi$, then $R$ will be a ring like $Z[\pi]$, which isn’t really an arithmetic subring of $C$. But, and this is the point, $R$ is still a finitely generated ring — you just forget that $\pi$ is a complex number and treat it as a free variable. The original system of equations has coefficients in $R$, and you can reduce the system modulo primes simply by applying any homomorphism from $R$ to a finite field. (They will always exist.) Then, as before, you can using arguments over finite fields (involving counting or Frobenius, say) to draw conclusions which you can then try to lift back to $R$ and then to $C$.

Unless I’m mistaken, this is how Grothendieck proved the the Ax-Grothendieck theorem. It says that if you have an injective map from the solution set of a system of complex polynomials to itself and the map is defined by polynomial equations, then the map is surjective. Over finite fields, the analogous statement is true by a counting argument, and over the complex numbers, you use the spreading technique. The reason this technique works really gets to the heart of what algebra is. It’s that in a system of polynomial equations, there are only finitely many symbols and hence only finitely many coefficients, even if those coefficients are transcendental. Therefore the ring $R$ is finitely generated, and therefore it has many maps to finite fields (and other rings).

So my second question is whether something similar happens in logic, or whether it could. Any theorem or proof involves only finitely many symbols, and could it be the case that you can consider the minimal logic over which it makes sense and then, since this logic has a finite nature, specialize it to some exotic, restrained logic where completely different techniques are available?

I don’t know if this is completely crazy, but I’m somewhat heartened by the fact that the other person who proved the Ax-Grothendieck theorem, namely Ax, gave a proof using logic.

(continued from the last comment.)
******
Suppose A is a sequence of symbols. Then A is a wff if there exists a sequence A1,…,An
(for some n ≥ 1) such that:
1) An is A
2) for every i (1≤i≤n),Ai is either:
a) a capital Roman letter; or
b) (not Aj), (Aj and Ak), (Aj or Ak), (Aj implies Ak), or (Aj if and only if Ak), for some j,k where 1 ≤ j,k and i > j,k.
******
Sorry, the copy-paste didn’t work perfectly in the last comment, so that’s the correct version.
******
A proof of S is then a sequence of wffs W1,…,Wn such that:

1) Wn is S
2) for every i (1≤i≤n), Wi is either:
a) an axiom; or
b) there exists j,k where i > j,k and Wj is (Wk implies Wi).
*******
That’s exactly the manner in which F defines its provability predicate, so it really does have one, and it really does prove its own consistency.
*******
Adding the row of stars seemed to do the trick to get the comment accepted. Apologies if it reduced the readability.

Jeffrey, hmmmm… I have now answered what you claimed to be the “central” issue. One does *not* assume that the language has a w-sequence of entities. Do you agree or not? Do you understand now that there is no incoherence in any of the claims?

“You wish to consider the consider the set of finite sequences up to length n over an alphabet A of size k…”

I don’t wish to do anything of the sort. That’s you talking, not me, trying to fit what I’m saying into a little box. One does not make any, and does not need to make any, assumption about the cardinality of F being finite or infinite, just as one does not make any assumptions about the cardinality of N.

So let’s just review your objections.

First, you claimed that F did not distinguish between syntactic entities. OK, after a few exchanges, you had an epiphany, and you now realize that F does, in fact, distinguish between entities, unless of course you’re back to meaning “distinguish” as “proving that the entity exists”.

Second, you claim that the philosophy behind F is incoherent. Now the philosophy behind F is an agnosticism about the Successor Axiom and whether N goes on and on forever. You claimed this was incoherent because the language has a w-sequence of entities. I presume now you understand that one does not make and does not need to make that assumption and so that the philosophy behind F is coherent.

Third, you claimed that, in any case, the system is “extreme and pointless.” Hmmm…. well, since the original question was about systems that can prove their own consistency, where’s the pointless? F proves its own consistency. And what’s more it’s a natural system, because it takes a well-known system, second-order deductive PA, and subtracts a few axioms. That’s about as natural as you get. And it does this and is *still* able to prove Quadratic Reciprocity and (probably) Fermat’s Last Theorem. That would, it seem, be a reasonably strong system which can prove its own consistency. Sounds interesting to me, but if you personally find it pointless, well, can’t argue with it, because pointlessness is in the eye of the beholder.

The only possible objection is actually the one that John mentioned, which is whether F really is able to talk about its own consistency. On this it’s obvious that it can - just look at how it formulates the predicate Provable(x). Consider the case of a propositional logic, which is simpler (and so I can explain it here). In my last comment I explained how one defines what is a wff in a propositional logic:

(to be continued…)