An additional constraint to the ZFC axioms?

[Stephen Tashi]

I am a bit confused. If that's the case then it seems one would have to regard a usual formal presentation of PA (and many other theories ...) as not being presented as a formal language.

In my limited experience, I haven't encountered any presentations of mathematical theories as purely formal languages. Those that I have seen employ propositional logic. By definition, there must be a mapping from propositions to truth values. By "formal language", I don't mean "formal" in sense of dignified or precise. I'm talking about a system that merely deals with the manipulation of symbolic expressions.

For example, a formal language might contain a rule that a string of three astericks can be replaced by a dollar sign. So beginning with "$a***b**c***d$" we can derive "$a\$b**c\$d$". There is no assertion that if "$a***b**c***d$" is mapped to the value "true" then "$ab**c\$d$" must also be mapped to the value "true". There is no assumption that a mapping from symbolic expressions to truth values must exist.

The notion of truth does enter into the metalanguage used in discussing formal languages. We do consider whether it is true that "$ab**c\$d$" can be derived from "$a***b**c***d$".

 

[PeterDonis]

I consider the presentation of something as a formal language not to include the assumption that there is a mapping that assigns each (well formed) symbolic expression a truth value - true or false. This does not preclude than an interpretation of the symbolic language might assume the existence of such a mapping.

I think I see what you might be getting at here, but let me rephrase it in what seems to me to be better terminology, and then see if you agree.

If we just consider a formal system in isolation, strictly speaking, we have a concept of "provable"--a set of well-formed formulas for which there is a proof using the rules of inference of the formal system. In Schuller's presentation, the rules of inference are that all tautologies are provable, all axioms are provable, and all formulas which can be derived via his rule M from provable formulas are provable. Any well-formed formula $F$ therefore falls into one of three categories: provable (meaning that there is a proof of formula $F$), falsifiable (meaning that there is a proof of formula $\neg F$), and undecidable (meaning that there is not a proof of either $F$ or $\neg F$).

To introduce the concept of "true", strictly speaking, we need to consider not just a formal system in isolation, but a formal system in conjunction with a semantic model. In any semantic model of a formal system, the following will be the case:

Any proposition corresponding to a provable formula is true.

Any proposition corresponding to a falsifiable formula is false.

Propositions corresponding to undecidable formulas fall into two categories: those which are true in this semantic model (but might be false in other semantic models of the same formal system), and those which are false in this semantic model (but might be true in other semantic models of the same formal system).

For example, as I pointed out in an earlier post, consider a semantic model of the formal system ZFC. In any such semantic model, it will be the case that there is an empty set (since that is an axiom of ZFC and therefore provable), and it will not be the case that there is a set whose power set is not also in the model (since that would contradict the power set axiom of ZFC, so the corresponding formula is falsifiable). However, there will be some semantic models of ZFC in which the continuum hypothesis is true, and others in which it is false, since the continuum hypothesis is undecidable in ZFC.

Notice that there are no propositions in any semantic model that are not either true or false. The only distinctions are between true propositions that correspond to provable formulas and true propositions that correspond to undecidable formulas, and between false propositions that correspond to falsifiable formulas and false propositions that correspond to undecidable formulas. So every well-formed formula corresponds to a proposition that has a definite truth value in whatever semantic model we are considering.

In informal language, this often gets stated as "all well-formed formulas have a definite truth value", and we think of the formulas themselves as being true or false instead of the propositions corresponding to them in a semantic model. Usually this is because we have some particular semantic model in mind and we are thinking solely in terms of that particular model. It might also sometimes be because we are not considering the possibility of multiple different semantic models at all.

 

[PeterDonis]

In my limited experience, I haven't encountered any presentations of mathematical theories as purely formal languages. Those that I have seen employ propositional logic.

But propositional logic is itself a formal language.

By definition, there must be a mapping from propositions to truth values.

In propositional logic taken by itself, no, there are just propositions and the three categories I described in my previous post: provable (which in the case of propositional logic taken by itself is just the tautologies), falsifiable (which is just the negations of tautologies), and undecidable (which is all other propositions).

Along the lines of my previous post, there is an obvious sense in which all the tautologies are "true" and all their negations are "false": that in any formal system which is built on propositional logic, all tautologies will always be provable (and therefore true in all semantic models) and all their negations will always be falsifiable (and therefore false in all semantic models). However, if we are considering just propositional logic by itself, we would have to pick a particular semantic model in order to assign truth values to the undecidable propositions--and of course, without additional structure over and above propositional logic, we would be free to pick our semantic model to give either truth value to any particular undecidable proposition.

 

[SSequence]

There are two different things (at a macro level so to speak). Let's focus on PA. So we have a finite (or countably finite) alphabet $\Sigma$ for forming the (finite) strings.

(1) One question would be whether it is decidable given a string whether it can be characterised "true/false" sentence or not [what I have in mind is well-formed-expression with no free variables]. The answer to this would be yes.

(2) The second question would be whether the theorems are recursively enumerable or not. The answer would again be yes.

====================

The issue you mentioned in post#34 is related to LEM. Now due to very nature of PA (classical logic) it assumes every question it asks to be either true or false. I am quite far from very well-informed here, but just about any theory which assumes "classical mode of inference all the way" in its background will assume LEM in its background [without any exception for all its true/false questions] and will not satisfy the kind of condition you mentioned in post#34.

I think when the underlying set of truths of a theory forms a recursive set [I will have to think about r.e.] assuming LEM shouldn't be any issue (should probably be true for number of theories weaker than PA). For PA, the set of its truths is of higher complexity.

====================

Regarding what is written in post#37, it is correct based upon model theory [and the results, at least as I have read, should be theorems of ZFC ... but I don't know to what extent the background assumptions can be weakened]. That is, according to model theory, in a given model each question posed by ZFC will have definite truth/false value. Also note that these results also apply to PA.

An interesting scenario is that [assuming $con(ZFC)$] in some model for sets, one will have ~$con(ZFC)$ as true, which is a consequence of second-incompleteness-theorem and points mentioned in post#37.

 

[PeterDonis]

Let's focus on PA.

What is PA?

One question would be whether it is decidable given a string whether it can be characterised "true/false" sentence or not [what I have in mind is well-formed-expression with no free variables].

I assume you mean "it is decidable whether a given string is well-formed", not "it is decidable whether a given well-formed string is true"?

The issue you mentioned in post#34 is related to LEM.

What is LEM?

 

[SSequence]

What is PA?

Peano arithmetic

I assume you mean "it is decidable whether a given string is well-formed", not "it is decidable whether a given well-formed string is true"?

Yeah you are right (it is just difference of words). I don't remember the exact terminology. What I meant was that, given a string, the problem of identifying whether it is a "question/problem" (to be answered) is decidable.

I didn't just write a well-formed-expression because I think that is also supposed to include formulas with free variables too? Though that would be decidable too.

Being able to decide both that
(i) given string forms a question/sentence
(ii) the answer to question is true
would only be possible in something weaker than PA.

What is LEM?

Law of Excluded Middle