4

Not on classical logic obviously since it validates excluded middle, but less obviously not on intuitionistic logic either. Intuitionists identify truth and provability and discard excluded middle, which sounds promising, but the unfortunate side effect of the latter is that many classically provable statements (like the intermediate value theorem) are no longer provable. For definiteness, consider classical mathematics and undecidable statements in the standard set theory (ZFC).

Here is the intuitive reason I think there should be some such logic. A nominalist/formalist may see classical mathematics as a useful game of symbols played by time tested rules, now formally codified. Excluded middle is one of the rules and is perfectly admissible, but if the rules can not determine the truth value of a statement, then that's it - there is no Platonic realm to reach into for a missing piece. Something like the continuum hypothesis simply has no truth value. As someone quipped, most mathematicians are Platonists, most non-mathematicians are nominalists, so this view may be widely held.

Such a view seems coherent to me and arguably delivers the best of both worlds: all of classical mathematics, none of Platonic baggage. Currently popular set theoretic pluralism essentially adopts it: "mathematical reality may be best understood as fractured and indeterminate", there is multiverse of set theories, many different rules, many different games.

At first glance it looks like one is using classical logic in the object language and intuitionistic logic in the meta-language. But I am not sure if that can be done consistently, or how the semantics would work. Also, on classical logic non-existence of objects trivializes mathematics since all conditionals are vacuously true, so some adjustment is needed. Is there a worked out logic that accomodates pluralism?

  • Every statement is decideable in some theories and undecideable in others, so I don't understand what you're asking for. – WillO Oct 6 '15 at 0:31
  • @WillO I am talking about classical math, i.e. ZFC, not some theories. – Conifold Oct 6 '15 at 0:40
  • It might good to say that in your question, which currently does not even mention ZFC. – WillO Oct 6 '15 at 0:44
  • Recall that the halting problem is unsolveable. And a lot of undecidable propositions are undecidable only because their solution procedures would run infinitely long. But we cannot detect which procedures will not stop. So they are undecidably undecidable. So you cannot know exactly which of your statements not to give truth-values to. At which point, what good does this notion do? – jobermark Oct 6 '15 at 16:03
  • @jobermark I don't follow how the halting problem is relevant. And we can not always know what is or isn't true either, but that doesn't preclude having a notion of truth. – Conifold Oct 7 '15 at 1:03
2

There is also another approach : Constructive Mathematics, and in particular Bishop's version, that provides :

a constructive development of a large part of twentieth-century analysis, including the Stone-Weierstrass Theorem, the Hahn-Banach and separation theorems, the spectral theorem for self-adjoint operators on a Hilbert space, the Lebesgue convergence theorems for abstract integrals, Haar measure and the abstract Fourier transform, [...].

See at least :

and :

  • Vow, constructive analysis has come a long way. But I thought that imposing strictures on classical reasoning is what made intuitionism and constructivism so unpopular. Is there a consistent way to allow excluded middle, choice, etc. in set theory without committing to them semantically? – Conifold Oct 6 '15 at 17:58
  • Bishop himself considers that a step in the process of mathematical development. It is just fine to classically prove stuff, but mathematics should not stop short of attempting constructive proof. Constructive proof provides much more than 'truth' it provides computational methods for handling all the objects involved. So even if you drop it as a requirement for 'truth', it should remain a goal. – jobermark Oct 7 '15 at 15:38
1

This should be some kind of paraconsistent logic. LInk to Stanford Encyclopedia entry here: http://plato.stanford.edu/entries/logic-paraconsistent/

Would be nice if someone could reference examples of any projects on this.The article points to research on something called inconsistent mathematics.

A nice overview of the issue is to be found in Priest's article , Mathematical Pluralism, Logic Jnl IGPL (2012) doi: 10.1093/jigpal/jzs018.

  • Paraconsistent logics exclude the Law of Non-contradiction. Therefore, they would exclude any classical theorems for which no proof currently exists other than a "proof by contradiction" method of proof, and any theorems which relied on such theorems. – Nick R Oct 6 '15 at 16:51
  • Point taken but the original question ruled out logics that accept the excluded middle hard to see how you can satisfy this without some form of paraconsistency. Meyer's R# relevance arithmetic seems like a basis for addressing the type of mathematics needed to address the points raised by the original question and this requires something along the lines of paraconsistent logic and inconsistent mathematics. I really don't see how one can get around this and satisfy all of the original question requirements. – Rodney Beard Oct 6 '15 at 19:59
  • Paraconsistent logics are meant to contain contradictions, but why would they arise here? Intuitionistic logic discards excluded middle without discarding non-contradiction, so one can be kept without the other. And I am asking for something that is only "partially" intuitionistic. – Conifold Oct 6 '15 at 20:30
  • I think the answer is to be found in the discussion in the article on inconsistent mathematics. In particular the arithmetic section on relevant arithmetic and Priests work on that and the section on the dual nature of relevant arithmetic and intuitionistic mathematics at the end of the analysis section plato.stanford.edu/entries/mathematics-inconsistent – Rodney Beard Oct 6 '15 at 23:50
  • Let me add that the intent of much of the development of inconsistent mathematics appears to very close to addressing the issues you raise. I could be wrong here, perhaps I have not understood the question, but it seems to me the above discussions largely raise the same issues as those addressed in the inconsistent math article and in Priest's article on mathematical pluralism. so I have the impression these are at least somewhat relevant here. – Rodney Beard Oct 6 '15 at 23:57
1

Provability logic will probably do the trick. Basically, provability logic takes the box in modal logic to represent provability in some system S. So you'd read S as the strongest foundational system you accept (ZFC or whatever). And you'd read "p is true" as "Box p" and "p is false" as "Box ~p." I don't know if this is a terribly principled way of going about things, but I'll leave the motivation up to you.

Edit: I do want to encourage you to relax the requirement that "undecidable statements are neither true nor false." If there's one thing we've learned over the past century, it's that truth and proof can come apart. And it's no better to tie (truth-or-falsity) to provability.

  • Interesting find, a modal logic that even Quine could swallow. But it seems that it is worked out only for S being versions of arithmetic, is there a problem with stronger theories? Playing nominalist's advocate though one could say that what we learned is that truth and proof coming apart is a price to pay for imagining objects behind mathematical symbols. Without standard models and intended interpretations, that are question begging against nominalists, even Godel sentences are not true but unprovable, they are neither true nor false. Or "true" as in provable in the second order arithmetic. – Conifold Oct 6 '15 at 17:34
  • Provability logic and the formalization of intuitionism are the same thing. The box isolates the redundant 'nots' forced on you by the loss of LEM in contexts that might not be finitely expressible. – jobermark Oct 7 '15 at 15:40
1

You mention 'set-theoretic pluralism', so you already know that standard classical logic, with the standard interpretation via model theory already is such a logic.

Those things that are true in all models of your axioms are true, those things that are true in no model are false. If you can create both a consistent model that contains an assertion and one that does not, then it is, by definition, neither true nor false, meeting neither criterion.

This already establishes all the things you ask about, including the semantics, which are determined by that definition of true and false. It also kind of prescribes how the logic 'works' -- one must mark out and set aside independent hypotheses as potential seed axioms and not use facts within the same proof or construction that require contradictory axiom collections.

So I miss the point of the question. I assumed you expected some kind of finite or transfinite proof-procedure for such a logic, but your responses indicate otherwise. Perhaps it is hidden in the motivation.

In this approach to modern set theory, one need not be constrained to anything as weak as intuitionism or constructivism in deductions or in the 'meta-language'. You can escape it in many ways, but two are obvious.

First, this definition of truth is based upon the construction of internally consistent example universes, and not on deduction. So things like the law of the excluded middle can be taken as axiomatic, and included as part of the definition of consistent. You need only 1) believe that isomorphic models really act the same and 2) give up the notion that there is a single over-arching meta-model of the entire universe which is internally consistent.

Second, you can stretch the notion of construction to some degree. The most basic models, L and V, include ordinals within the models. This gives you transfinite induction and, therefore, transfinite proof theory, which allows for 'constructive' proofs about a wider range of things. Given that convention, you can presume a tower of 'large cardinal axioms' reaching up to Woodin's 'Ulitmate L' which increase the power of infinite proofs by using the idea that one of the 'union steps' in any transfinite deduction will happen over a witness to the presumed axiom.

Also, I am not claiming the logic of model theory is free of confusion, only that it does, in fact, exist. One bizarre aspect of the semantics here that you call out by labeling the two layers is that the model construction happens in one set theory while the models themselves represent instances of another.

For instance, "the axiom of determinacy of infinite games" contradicts the axiom of choice. Studying the axiom of determinacy, we can create a space of models of it. Then in all those models the axiom of choice is necessarily false. But we create them embedded in a world where we assume the axiom of choice is true, and the semantics of models' existence allow for it. The semantics say, then, that the embedded proofs require it to be false, but our knowledge of those proofs is contingent upon it being potentially true. We do so because the universe where it is false has less freedom, so we are entertaining a superset of the models that would matter if it happened to be false. If the extra one's aren't real, no loss of credibility ensues.

But what if we did the opposite? We would have truths about the axiom of choice knowable only subject to its falsehood. The semantics admit such a thing, but whether it has any real meaning is highly questionable.

So far, we have amazingly found that our identified independent axioms clearly have a 'bigger' and a 'smaller' side, or they form 'towers' of freedom, like the tower of large cardinal axioms, or the tower that has "finitism, determinacy, projective determinacy, hierarchical determinacy, hierarchical choice, ramified choice, choice" and clearly goes from smaller to larger worlds.

They somehow do not have confluence points where it becomes ambigous which version of the world would 'admit more models'. But surely that is simply the human lack of imagination at work? It seems unreasonably convenient.

  • Good point, shows how a Platonist can interpret a nominalist, but does not work the other way, I am afraid. A model of ZFC is an assignment of truth values to all well-formed sentences. Without Platonically imagined universe there is no such thing. To a nominalist ZFC has no models, and quantification over "all models" is even more problematic. So this interpretation introduces more Platonic baggage than one had, and tried to avoid to begin with. But the meta-logic here is non-classical, it is a modal logic with models as possible worlds and truth equated to necessity. – Conifold Oct 12 '15 at 1:25
  • A model is less than a possible world, enough less that most formalists accept this model of reasoning. To begin with, the assignment of truth-values to statements in a model does not have to cover all statements, and it does not have to represent 'truth' beyond not contradicting the axioms. – jobermark Oct 12 '15 at 19:11
  • Otherwise, the incompleteness theorem would pretty much ban models of arithmetic, or analysis, which folks use all the time. We know we cannot assign some statements truth values. So why would we bother to consider only complete assignments of truth values, all zero of them? – jobermark Oct 12 '15 at 19:20
  • Incompleteness theorem does not limit truth valuation in Platonistic models, it only limits what can be proved in first order systems. Formalists do accept model theory, but to them a model of a theory is another theory, embedded into set theory (ZFC+), not a set. This would not work for your semantics since truth values of all sentences in all models have to be available for quantification. I guess the idea is to interpret ZFC nominalistically first, then extend it to model theory. That means that concepts of model theory can't be used in interpreting ZFC. – Conifold Oct 12 '15 at 23:56
  • OK, but the incompleteness of FOL indicates we should not rely upon total assignment of truth values. If we accepted the ability to totally fill in the semantics with truth values, people would not pursue independence results. We would not need this whole layer of relativization between two set theories, we would pursue a single model without gaps. And neither of the set theories being relativized has to be ZFC, so no, starting from a nominalization of ZFC is not the approach. The approach is to make models of one set theory in another set theory. – jobermark Oct 13 '15 at 16:04
1

The excluded middle does not imply everything is either true or false. For example, there is the four-valued logic whose truth values are (T,T), (T,F), (F,T), and (F,F), and the logical connectives are applied elementwise.

In this logic, (T,T) is true and (F,F) is false, but you still have those other two truth values, and they do still satisfy the law of the excluded middle; e.g. if we plug P=(T,F) into "P or not P", we compute

  • (T,F) or not (T,F)
  • (T,F) or (F,T)
  • (T,T)

It turns out there is a simple formal thing you can do; define a multi-valued logic whose truth values are precisely the equivalence classes of statements, where P and Q denote the same truth value if and only if there exists a proof of Q from P and a proof of P from Q.

In this logic, a statement is true if and only if it is a tautology; this includes all theorems of mathematics, like "Peano's axioms imply that 1+1=2".

Similarly, every contradiction is false.

Statements like "ZFC implies CH" will thus be neither true nor false.

And despite the multi-valued semantics, this is still classical logic, satisfying the law of the excluded middle: e.g. "P or not P" is a tautology, and consequently true.

There are ways one can reasonably interpret this as a space of "all possible mathematical worlds"; e.g. to view the relation that "(ZFC implies CH)≡true" as an equation that carves out the subspace of the whole 'universe' where the continuum hyptohesis holds.

0

I. It would be a very odd thing indeed if the truth/falsity/neither of a statement about, say, arithmetic could depend on a bunch of more-or-less-arbitrary axioms invented by human beings in the twentieth century.

This suggests, for example, that Gauss, who had never heard of ZFC, would have had no way of knowing that the statement "2+2=4" is true, and in fact would not have been able to formulate a correct definition of what it would mean for that statement to be true.

II. A given mathematical statement can have more than one formalization in ZFC, and it's possible for one of these formalizations to be decideable and the other not. On your account, do such statements have truth values?

III. It is, in any event, unclear what you're suggestion. Which of the following comes closest?

Version 1: Decideability in ZFC causes statements to have truth values.

Version 2: The set of statements that are decideable in ZFC happens to coincide with the set of statements that have truth values.

Version 3: Some other thing.

IV. You write: "if the rules can not determine the truth value of a statement, then that's it" --- Ah. But the question "Does Theorem A follow from Axioms B, C and D?" is a mathematical question, and you've just allowed that it has an answer. That means, given the rest of your program, that you are assuming that the statement "Theorem A follows from Axioms A, B, and C" is decideable. But we know that there are statements of that form that are not decideable. So I believe you are hoist on your own petard.

  • ZFC axioms are hardly arbitrary, they are distilled from centuries of successful use, including by Gauss. But you misunderstand, this is not my program or suggestion, I am just interested how one can logically combine different principles in object theory and interpretation in this example. Also, there is no need to assume that all decidability questions have answers to say that undecidable statements are neither true nor false, just as there is no need to know truth values of all sentences to say that they have them. Which sentences have truth values depends on one's notion of truth, so #3. – Conifold Oct 6 '15 at 17:50
  • " A given mathematical statement can have more than one formalization in ZFC, and it's possible for one of these formalizations to be decideable and the other not" Can you provide an example? – barrycarter Mar 17 '16 at 2:35

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.