Abstract
Solutions to semantic paradoxes often involve restrictions of classical logic for semantic vocabulary. In the paper we investigate the costs of these restrictions in a model case. In particular, we fix two systems of truth capturing the same conception of truth: (a variant) of the system KF of Feferman (The Journal of Symbolic Logic, 56, 1β49, 1991) formulated in classical logic, and (a variant of) the system PKF of Halbach and Horsten (The Journal of Symbolic Logic, 71, 677β712, 2006), formulated in basic De Morgan logic. The classical system is known to be much stronger than the nonclassical one. We assess the reasons for this asymmetry by showing that the truth theoretic principles of PKF cannot be blamed: PKF with induction restricted to non-semantic vocabulary coincides in fact with what the restricted version of KF proves true.
Similar content being viewed by others
Notes
These conditions are somewhat simplified. Besides numerals \(\phantom {\dot {i}\!}{\ulcorner \varphi \urcorner }\) for (codes of) sentences there will also be other closed terms with the code of Ο as their value. So the clause should be: A sentence T t is true iff the value of t is (the code of) a true sentence. Or one closes also under substitution of identicals. For the sake of the introduction here, we decided not to clutter the truth and falsity conditions with these subtleties.
In (IND), x is not free in \(\phantom {\dot {i}\!}\Gamma , \Delta , \varphi (\overline 0)\) and t is arbitrary.
Fischer et al. [5] study the criterion of Ο-categoricity in depth and consider also other criteria such as similarity with a semantic construction and proof theoretic strength that are, in many respect, less refined than categoricity for Ο-models. Having said that, it is also clear that Ο-categoricity can at best be a necessary condition for an axiomatic theory to capture a semantic construction: by replacing the truth theoretic axioms of PKF with sequents of the form \(\phantom {\dot {i}\!}T\ulcorner \varphi \urcorner \Rightarrow \varphi \) and \(\phantom {\dot {i}\!}\varphi \Rightarrow T\ulcorner \varphi \urcorner \), in fact, one obtains again an Ο-categorical axiomatization of Kripkeβs theory.
This result extends to the cases in which S is a consistent or a complete fixed point and (CONS) or (COMP) are added to KF, as we shall see in Section 5.
Cantini [2] introduced the system BT, although his definition differs slightly from the one adopted here.
For a definition of the systems of ramified truth up to the Feferman-SchΓΌtte ordinal Ξ0, see [6, Section 9].
For a definition of the Veblen functions, see again [6, Section 9].
KF βΎ is in fact conservative over PA. Any model of \(\phantom {\dot {i}\!}\mathcal {M}\) of PA can be expanded to a model \(\phantom {\dot {i}\!}(\mathcal {M},S_{1},S_{2})\) of KF βΎ where (S 1,S 2) is a fixed point of Ξ¦. This also yields the conservativity of PKF over PA as if PKF βΎ proved some formula Ο of \(\phantom {\dot {i}\!}\mathcal {L}\) not provable in PA, Ο would also be provable in KFr by the monotonicity of the logic DM.
The picture that arises from our result is complemented by the results in [15], in which it is shown that PKF=IBT and that IKF=PKF plus transfinite induction up to Ξ΅ 0.
Equivalently, restriction to the least number principles or to forms of collection.
See also [6, chapter 20].
By writing β\(\phantom {\dot {i}\!}\mathcal M\) is a model of \(\phantom {\dot {i}\!}\mathcal S\)β we mean that \(\phantom {\dot {i}\!}\mathcal M\) is a model of its derivable sequents.
Of course in the other case in which we focus on Ξ+, the Lemma would need to be suitably modified.
The positive complexity of a formula Ο of \(\phantom {\dot {i}\!}\mathcal L\) is 0 for atomic and negated atomic sentences; and n+1 for sentences of the form ¬¬Ο,Οβ§Ο,βx Ο with n the maximum of the complexities of Ο and Ο.
References
Blamey, S. (2002). Partial logic. In Gabbay, D., & Guenther, F. (Eds.) Handbook of philosophical logic. 2nd edn., (Vol. 5 pp. 261β253). Dordrecht: Kluwer.
Cantini, A. (1989). Notes on formal theories of truth. ZeitSchrift fΓΌ,r matematische Logik und Grundlagen der Mathematik, 35, 97β130.
Feferman, S. (1991). Reflecting on incompleteness. The Journal of Symbolic Logic, 56, 1β49.
Field, H. (2008). Saving truth from paradox. Oxford: Oxford University Press.
Fischer, M, Halbach, V., Kriener, J., & Stern, J. (2015). Axiomatizing semantic theories of truth. The Review of Symbolic Logic, 8(02), 257β278.
Halbach, V. (2014). Axiomatic theories of truth. CUP.
Fujimoto, K. (2010). Relative truth definability of axiomatic theories of truth. The Bulletin of Symbolic Logic, 16, 305β344.
Halbach, V., & Horsten, L. (2006). Axiomatizing kripkeβs theory of truth. The Journal of Symbolic Logic, 71, 677β712.
Horsten, L. (2009). Levity. Mind, 118, 555β581.
Horsten, L. (2012). The Tarskian turn: deflationism and axiomatic truth, (p. 2012). Princeton: Princeton University Press.
Kremer, M. (1988). Kripke and the logic of truth. Journal of Philosophical Logic, 17, 225β278.
Kripke, S. (1975). Outline of a theory of truth. Journal of Philosophy, 72, 690β712.
McGee, V. (1991). Truth, vagueness and paradox: an essay in the logic of truth. Cambridge: Hackett.
Moschovakis, Y. (1974). Elementary induction on abstract structures. Amsterdam: North-Holland.
Nicolai, C. Provably true sentences across axiomatizations of Kripkeβs theory of truth. Unpublished manuscript.
Reinhardt, W. (1986). Some remarks on extending and interpreting theories with a partial predicate for truth. Journal of Philosophical Logic, 15, 219β251.
Scott, D. (1975). Combinators and classes. In BΓΆhm, C. (Ed.) Ξ»-calculus in computer science, (Vol. 1975 pp. 1β26). Berlin: Springer.
Williamson, T. (2016). Semantic paradoxes and abductive methodology. To appear in: Armour-Garb, B. (forthcoming). The Relevance of the Liar. Oxford University Press.
Acknowledgments
We would like to thank Leon Horsten and an anonymous referee. The work of the second author was supported by the European Commission, Grant 658285 FOREMOTIONS.
Author information
Authors and Affiliations
Corresponding author
Appendices
Appendix 1: The logic DM
The initial sequents of the system DM are:
In (Β¬), ¬Πdenotes the set of all negations of sentences in Ξ. In ( β1) and ( β2), x is not free in the lower sequent.
Classical logic K is obtained by replacing, in DM, ( Β¬) with the stronger
Appendix 2: Axioms of KF
PAT is the theory formulated in K (cf. Appendix 1) extended with initial sequents βΟ, for Ο a basic axiom of PA, and the induction rule
with x not free in \(\phantom {\dot {i}\!}\Gamma ,\Delta ,\varphi (\overline 0)\) and t arbitrary, for all formulas Ο of \(\phantom {\dot {i}\!}\mathcal {L}_{T}\). KF is obtained from PAT by adding the following initial sequents, where s,t range over (codes of) closed terms of \(\phantom {\dot {i}\!}\mathcal {L}_{T}\):
- KF1:
-
-
1.
\(\phantom {\dot {i}\!}{s^{\circ }}={t^{\circ }}\Rightarrow \textit {T}(\textit {s}\underset {\cdot }{=}\textit {t})\) (where (β )β is the arithmetical evaluation function)
-
2.
\(\phantom {\dot {i}\!} \textit {T}(\textit {s}\underset {\cdot }{=}\textit {t})\Rightarrow {s^{\circ }}={t^{\circ }}\)
-
1.
- KF2:
-
-
1.
\(\phantom {\dot {i}\!}{s^{\circ }}\neq {t^{\circ }}\Rightarrow \textit {T}(\underset {\cdot }{\neg }\, s= t)\)
-
2.
\(\phantom {\dot {i}\!}\textit {T}(\underset {\cdot }{\neg }\, s= t)\Rightarrow {s^{\circ }}\neq {t^{\circ }}\)
-
1.
- KF3:
-
-
1.
\(\phantom {\dot {i}\!}{\text {Sent}_{\mathcal {L}_{T}}}(x),\textit {T}\,\underset {\cdot }{\neg }\underset {\cdot }{\neg }\,x\Rightarrow \textit {T}x\)
-
2.
\(\phantom {\dot {i}\!}{\text {Sent}_{\mathcal {L}_{T}}}(x),\textit {T}x\Rightarrow \textit {T}\,\underset {\cdot }{\neg }\underset {\cdot }{\neg }\,x\)
-
1.
- KF4:
-
-
1.
\(\phantom {\dot {i}\!}{\text {Sent}_{\mathcal {L}_{T}}}(x\underset {\cdot }{\land }y), \textit {T}(x\underset {\cdot }{\land }y)\Rightarrow \textit {T}x\land \textit {T}y\)
-
2.
\(\phantom {\dot {i}\!}{\text {Sent}_{\mathcal {L}_{T}}}(x\underset {\cdot }{\land }y), \textit {T}x\land \textit {T}y\Rightarrow \textit {T}(x\underset {\cdot }{\land }y)\)
-
1.
- KF5 :
-
-
1.
\(\phantom {\dot {i}\!}{\text {Sent}_{\mathcal {L}_{T}}}(x\underset {\cdot }{\land }y),\textit {T}\underset {\cdot }{\neg }(x \underset {\cdot }{\land }y)\,\Rightarrow \,\textit {T}\,\underset {\cdot }{\neg } x\vee \textit {T}\,\underset {\cdot }{\neg } y\)
-
2.
\(\phantom {\dot {i}\!}{\text {Sent}_{\mathcal {L}_{T}}}(x\underset {\cdot }{\land }y),\textit {T}\,\underset {\cdot }{\neg } x\vee \textit {T}\,\underset {\cdot }{\neg } y\,\Rightarrow \,\textit {T}\,\underset {\cdot }{\neg }\,(x\underset {\cdot }{\land }y)\)
-
1.
- KF6:
-
-
1.
\(\phantom {\dot {i}\!}{\text {Sent}_{\mathcal {L}_{T}}}(x\underset {\cdot }{\vee }y), \textit {T}(x\underset {\cdot }{\vee }y)\Rightarrow \textit {T}x\vee \textit {T}y\)
-
2.
\(\phantom {\dot {i}\!}{\text {Sent}_{\mathcal {L}_{T}}}(x\underset {\cdot }{\vee }y), \textit {T}x\vee \textit {T}y\Rightarrow \textit {T}(x\underset {\cdot }{\vee }y)\)
-
1.
- KF7 :
-
-
1.
\(\phantom {\dot {i}\!}{\text {Sent}_{\mathcal {L}_{T}}}(x\underset {\cdot }{\vee }y),\textit {T}\,\underset {\cdot }{\neg }\,(x \underset {\cdot }{\vee }y)\,\Rightarrow \,\textit {T}\,\underset {\cdot }{\neg } x\land \textit {T}\,\underset {\cdot }{\neg } y\)
-
2.
\(\phantom {\dot {i}\!}{\text {Sent}_{\mathcal {L}_{T}}}(x\underset {\cdot }{\vee }y),\textit {T}\,\underset {\cdot }{\neg } x\land \textit {T}\,\underset {\cdot }{\neg } y\,\Rightarrow \,\textit {T}\,\underset {\cdot }{\neg }\,(x\underset {\cdot }{\vee }y)\)
-
1.
- KF8:
-
-
1.
\(\phantom {\dot {i}\!}{\text {Sent}_{\mathcal {L}_{T}}}(\underset {\cdot }{\forall } vx),\forall t\,\textit {T}(x(t/v))\Rightarrow \textit {T}(\underset {\cdot }{\forall } vx)\)
-
2.
\(\phantom {\dot {i}\!}{\text {Sent}_{\mathcal {L}_{T}}}(\underset {\cdot }{\forall } vx),\textit {T}(\underset {\cdot }{\forall } vx)\Rightarrow \forall t\,\textit {T}(x(t/v))\)
-
1.
- KF9:
-
-
1.
\(\phantom {\dot {i}\!}{\text {Sent}_{\mathcal {L}_{T}}}(\underset {\cdot }{\forall } vx),\exists t\,\textit {T}(\underset {\cdot }{\neg } x(t/v))\Rightarrow \textit {T}(\underset {\cdot }{\neg }\,\underset {\cdot }{\forall } vx)\)
-
2.
\(\phantom {\dot {i}\!}{\text {Sent}_{\mathcal {L}_{T}}}(\underset {\cdot }{\forall } vx),\textit {T}(\underset {\cdot }{\neg }\,\underset {\cdot }{\forall } vx)\Rightarrow \exists t\,\textit {T}(\underset {\cdot }{\neg } x(t/v))\)
-
1.
- KF10:
-
-
1.
\(\phantom {\dot {i}\!}{\text {Sent}_{\mathcal {L}_{T}}}(\underset {\cdot }{\exists } vx),\exists t\,\textit {T}(x(t/v))\Rightarrow \textit {T}(\underset {\cdot }{\exists } vx)\)
-
2.
\(\phantom {\dot {i}\!}{\text {Sent}_{\mathcal {L}_{T}}}(\underset {\cdot }{\exists } vx),\textit {T}(\underset {\cdot }{\exists } vx)\Rightarrow \exists t\,\textit {T}(x(t/v))\)
-
1.
- KF11:
-
-
1.
\(\phantom {\dot {i}\!}{\text {Sent}_{\mathcal {L}_{T}}}(\underset {\cdot }{\exists } vx),\forall t\,(\textit {T}\,\underset {\cdot }{\neg } x(t/v))\Rightarrow \textit {T}(\underset {\cdot }{\neg }\,\underset {\cdot }{\exists } vx)\)
-
2.
\(\phantom {\dot {i}\!}{\text {Sent}_{\mathcal {L}_{T}}}(\underset {\cdot }{\exists } vx),\textit {T}(\underset {\cdot }{\neg }\,\underset {\cdot }{\exists } vx)\Rightarrow \forall t\,(\textit {T}\,\underset {\cdot }{\neg } x(t/v))\)
-
1.
- KF12:
-
-
T t ββTαΉ¬ t
-
- KF13:
-
-
\(\phantom {\dot {i}\!}\textit {T}\underset {\cdot }{\neg }\,\textit {\d {T}}t\Leftrightarrow \textit {T}\underset {\cdot }{\neg }\,{t^{\circ }}\vee \neg {\text {Sent}_{\mathcal {L}_{T}}}({t^{\circ }})\)
-
- KF14:
-
-
\(\phantom {\dot {i}\!}\textit {T}x\Rightarrow {\text {Sent}_{\mathcal {L}_{T}}}(x)\)
-
KF βΎ is obtained by restricting (IND) to formulas of \(\phantom {\dot {i}\!}\mathcal {L}\) and adding the sequents (Reg1) and (Reg2). We consider the extension of KF β that we call KFββ KFβ β via the disjunction of the following sentences, forcing complete or consistent extensions of the truth predicate respectively:
Appendix 3: Completeness of DM
The bulk of this appendix is to prove Proposition 4 below. We recall that we write \(\Gamma \vDash _{\mathcal S} \Delta \) to mean that for all four-valued models \(\mathcal M\) of a set of sequents and rules \(\mathcal S\supseteq \textsf {DM}\), the following are jointly satisfied:Footnote 15
-
if \(\phantom {\dot {i}\!}\mathcal M\vDash _{\textsf {DM}} \varphi \) for all ΟβΞ, then \(\phantom {\dot {i}\!}\mathcal M\vDash _{\textsf {DM}} \psi \) for at least one ΟβΞ;
-
if \(\phantom {\dot {i}\!}\mathcal M\vDash _{\textsf {DM}}\neg \psi \) for all ΟβΞ, then \(\phantom {\dot {i}\!}\mathcal M\vDash _{\textsf {DM}}\neg \varphi \) for at least one ΟβΞ.
For notational simplicity, we do not deal with variable assignments.
The informal sketch of the strategy is as follows: we start with a pair (Ξ,Ξ) such that ΞβΞ is not derivable in \(\phantom {\dot {i}\!}\mathcal S\), and build βmaximalβ sets Ξ+ and Ξ+ such that Ξ+βΞ+ is still not \(\phantom {\dot {i}\!}\mathcal S\)-derivable. We can in fact extend our notion of derivability (and underivability) in DM to sequents ΞβΞ where Ξ,Ξ are infinite: \(\mathcal S\vdash {\Lambda }\Rightarrow {\Theta }\) iff for some finite Ξβ²βΞ, Ξβ²βΞ, we have \(\phantom {\dot {i}\!}\mathcal S\vdash {\Lambda }^{\prime }\Rightarrow {\Theta }^{\prime }\). From Ξ+,Ξ+ a four-valued model \(\phantom {\dot {i}\!}\mathcal M\) of \(\phantom {\dot {i}\!}\mathcal S\) can be then read off, one that satisfies at least one of the following:
-
if \(\phantom {\dot {i}\!}\mathcal M\vDash _{\textsf {DM}}\varphi \) for all ΟβΞ+, then \(\phantom {\dot {i}\!}\mathcal M\nvDash _{\textsf {DM}} \psi \) for ΟβΞ+;
-
if \(\phantom {\dot {i}\!}\mathcal M\vDash _{\textsf {DM}}\neg \psi \) for all ΟβΞ+, then \(\phantom {\dot {i}\!}\mathcal M\nvDash _{\textsf {DM}} \neg \varphi \) for ΟβΞ+.
Henkin-style arguments of the kind given below can be found in [11] for a different sequent calculus and in [13] for a system of natural deduction. [1] hints at a more general strategy.
Proposition 4
Let \(\phantom {\dot {i}\!}\mathcal S\) be a set of sequents in a language \(\phantom {\dot {i}\!}\mathcal L\) and Ξ,Ξ finite sets of \(\phantom {\dot {i}\!}\mathcal L\) -formulas. Then:
We prove the counterpositive. If \(\phantom {\dot {i}\!}\nvdash _{\mathcal S} \Gamma \Rightarrow \Delta \), by (Cut), there cannot be a Ο such that
Let \(\phantom {\dot {i}\!}\mathcal L^{+}:=\mathcal L\cup C\) the language \(\phantom {\dot {i}\!}\mathcal L\) expanded with a countable set of new constants. Let {Ο n | nβΟ} and {c i | iβΟ} enumerations of the formulae of \(\phantom {\dot {i}\!}\mathcal L^{+}\) and constants in C respectively.
Next we inductively define Ξ+ and Ξ+ as follows:
-
Ξ0:=ΞandΞ0:=Ξ
-
if \(\phantom {\dot {i}\!}\nvdash _{\mathcal S}\Gamma _{n},\varphi _{n}\Rightarrow \Delta _{n}\), then Ξ n+1=Ξ n and
$$\Gamma_{n+1}:= \left\{\begin{array}{ll} &\Gamma_{n}\cup\{\varphi_{n},\chi(c_{i}/x)\},\hspace{10pt}\text{if }\varphi_{n}\text{ is }\exists x\chi\text{ and }c_{i}\text{ is the least constant in }C\\ &\hspace{100pt} \text{not occurring in }\Gamma_{n},\Delta_{n},\varphi_{n}.\\ &\Gamma_{n}\cup\{\varphi_{n},\neg\chi(c_{i}/x)\},\hspace{10pt}\text{if }\varphi_{n}\text{ is }\neg\forall x\chi\text{ and }c_{i}\text{ the least constant in }C\text{ not}\\ &\hspace{100pt}\text{ occurring in }\Gamma_{n},\Delta_{n},\varphi_{n}.\\ &\Gamma_{n}\cup\{\varphi_{n}\},\hspace{50pt}\text{otherwise} \end{array}\right. $$ -
if \(\phantom {\dot {i}\!}\vdash _{\mathcal S}\Gamma _{n},\varphi _{n}\Rightarrow \Delta _{n}\), we have Ξ n+1=Ξ n and
$$\Delta_{n+1}= \left\{\begin{array}{ll} &\Delta_{n}\cup\{\varphi_{n},\chi(c_{i}/x)\},\hspace{10pt}\text{if }\varphi_{n}\text{ is }\forall x\chi\text{ and }c_{i}\text{ is the least constant in }C\text{ not}\\ &\hspace{100pt}\text{ occurring in }\Gamma_{n},\Delta_{n},\varphi_{n}.\\ &\Delta_{n}\cup\{\varphi_{n},\neg\chi(c_{i}/x)\},\hspace{10pt}\text{if }\varphi_{n}\text{ is }\neg\exists x\chi\text{ and }c_{i}\text{ the least constant in }C\text{ not}\\ &\hspace{100pt}\text{ occurring in }\Gamma_{n},\Delta_{n},\varphi_{n}.\\ &\Delta_{n}\cup\{\varphi_{n}\},\hspace{60pt}\text{otherwise} \end{array}\right. $$
Let \(\phantom {\dot {i}\!}\Gamma ^{+}=\bigcup _{n\in \omega }\Gamma _{n}\) and \(\phantom {\dot {i}\!}\Delta ^{+}=\bigcup _{n\in \omega }\Delta _{n}\). Obviously we have ΞβΞ+ and ΞβΞ+.
Next we state some properties of the pair (Ξ+,Ξ+).
Lemma 9
-
1.
If Ξ β² βΞ + , Ξ β² βΞ + , with Ξ β² ,Ξ β² finite, and \(\phantom {\dot {i}\!}\mathcal S\vdash \Gamma ^{\prime }\Rightarrow \Delta ^{\prime }\) , then there is an nβΟ such that
$$\mathcal S\vdash \Gamma_{n}\Rightarrow \Delta_{n}$$ -
2.
\(\phantom {\dot {i}\!}\nvdash _{\mathcal S}\Gamma _{n}\Rightarrow \Delta _{n}\) for all n;
-
3.
\(\phantom {\dot {i}\!}\Gamma ^{+}\cap \Delta ^{+}=\varnothing \)
-
4.
t=tβΞ + and tβ tβΞ +;
-
5.
If ΟβΞ + , then \(\phantom {\dot {i}\!}\vdash _{\mathcal S}\Gamma ^{+}\cup \{\varphi \}\Rightarrow \Delta ^{+}\) (symmetrically for ΟβΞ +);
-
6.
s=tβΞ + and Ο(s/x)βΞ + , then Ο(t/x)βΞ +;
-
7.
sβ t and Ο(s/x)βΞ + , then Ο(t/x)βΞ +;
-
8.
s=tβΞ + if and only if sβ tβΞ +;
-
9.
there is no \(\phantom {\dot {i}\!}\varphi \in \mathcal L^{+}\) such that
$$\Gamma^{+}\Rightarrow\Delta^{+},\varphi\text{ and }\varphi,\Gamma^{+}\Rightarrow\Delta^{+}. $$
A four-valued model \(\phantom {\dot {i}\!}\mathcal M\) can now be defined as follows:
where
that is the equivalence class of terms of \(\phantom {\dot {i}\!}\mathcal L^{+}\) determined by s = tβΞ+. Moreover,
The term model \(\phantom {\dot {i}\!}\mathcal M\) so-defined enables us to prove the following lemma, which will in turn yields the desired result:Footnote 16
Lemma 10
For all \(\phantom {\dot {i}\!}\varphi \in \mathcal L^{+}\),
-
1.
ΟβΞ + if and only if \(\phantom {\dot {i}\!}\mathcal M\vDash _{\textnormal {\textsf {DM}}}\varphi \);
-
2.
if ΟβΞ + , then \(\phantom {\dot {i}\!}\mathcal M\nvDash _{\textnormal {\textsf {DM}}}\varphi \).
Proof
By induction on the positive complexity of Ο.Footnote 17 We mostly focus on the base and on the existential quantifier cases.
- Case 1::
-
Ο:= (s = t). (s = t)βΞ+ iff [ [s] ]=[ [t] ] iff \(\phantom {\dot {i}\!}\mathcal M\vDash _{\textsf {DM}} s=t\). If (s = t)βΞ+ and \(\phantom {\dot {i}\!}\mathcal M\vDash _{\textsf {DM}} s=t\), then [ [s] ]=[ [t] ] and s = tβΞ+, which would imply the \(\phantom {\dot {i}\!}\mathcal S\)-derivability of Ξ+βΞ+, against Lemma 9.
- Case 2::
-
Ο:= (sβ t). If (sβ t)βΞ+, by Lemma 9(8), s = tβΞ+. By Lemma 9(2), s = tβΞ+, therefore [ [s] ]β [ [t] ] and \(\phantom {\dot {i}\!}\mathcal M\vDash _{\textsf {DM}} s\neq t\). If sβ tβΞ+, again by Lemma 9(8), s = tβΞ+ and so \(\phantom {\dot {i}\!}\mathcal M\nvDash _{\textsf {DM}} s\neq t\).
- Case 3::
-
Ο: = P(t 1,...,t n ). By construction of \(\phantom {\dot {i}\!}\mathcal M\), ΟβΞ+ iff \(\phantom {\dot {i}\!}([\![t_{1}]\!],...,[\![t_{n}]\!])\in P_{\mathcal M}^{+}\), that is \(\phantom {\dot {i}\!}\mathcal M\vDash _{\textsf {DM}} P(t_{1},\ldots ,t_{n})\). If P(t 1,...,t n )βΞ+, then by Lemma 9(3), P(t 1,...,t n )βΞ+; therefore \(\phantom {\dot {i}\!}([\![t_{1}]\!],...,[\![t_{n}]\!])\notin P_{\mathcal M}^{+}\).
- Case 4::
-
Ο:=Β¬ P(t 1,β¦,t n ). Similar to the previous one.
- Case 5::
-
Ο:=¬¬Ο. Itβs easy to check that ΟβΞ+ iff ΟβΞ+ (otherwise Ξ+,ΟβΞ+ or Ξ+,¬¬ΟβΞ+ by Lemma 9, thus Ξ+βΞ+ by the DM-rules). We can then apply the induction hypothesis.
If ΟβΞ+, then ΟβΞ+ (otherwise Ξ+βΟ,Ξ+, and thus Ξ+βΞ,Ο). Again we apply the induction hypothesis.
- Case 6::
-
Ο:=βv i Ο.
By construction of Ξ+, ΟβΞ+ if and only if Ο(c)βΞ+ for suitable c. This is then equivalent to \(\phantom {\dot {i}\!}\mathcal M\vDash _{\textsf {DM}}\chi (c)\) and \(\phantom {\dot {i}\!}\mathcal M\vDash _{\textsf {DM}} \exists v_{i}\chi \) by induction hypothesis and definition of \(\phantom {\dot {i}\!}\vDash _{\textsf {DM}}\).
If ΟβΞ+, then Ο(t/v i )βΞ+ for any t (otherwise \(\vdash _{\mathcal S}\Gamma ^{+}\Rightarrow \Delta ^{+},\chi (t/v_{i})\) , by Lemma 9 and \(\vdash _{\mathcal S} \Gamma ^{+}\Rightarrow \Delta ^{+}\) since \(\mathcal S\vdash \chi (t)\Rightarrow \exists v\chi \) ). By induction hypothesis, \(\mathcal M\nvDash _{\textsf {DM}} \chi (t/v_{i})\).
- Case 7::
-
Ο:=Β¬ βv i Ο. If ΟβΞ+, then Β¬Ο(t/v i )βΞ+ for any t (as Β¬Ο(t)βΞ+ for some t entails \(\phantom {\dot {i}\!}\mathcal S\vdash \Gamma ^{+},\varphi \Rightarrow \Delta ^{+}\), thus Ξ+βΞ+, quod non). Also, if Β¬Ο(t/v i )βΞ+ for any t, then Β¬βv i ΟβΞ+ (as if ΟβΞ+, then ΟβΞ+, thus Β¬Ο(c)βΞ+ for suitable cβC). By induction hypothesis, this is equivalent to \(\phantom {\dot {i}\!}\mathcal M\vDash _{\textsf {DM}} \neg \chi (t)\) for any t and \(\phantom {\dot {i}\!}\mathcal M\vDash _{\textsf {DM}}\varphi \).
By definition of Ξ+, if ΟβΞ+, then Β¬Ο(c/v i )βΞ+ for suitable cβC. By induction hypothesis, \(\phantom {\dot {i}\!}\mathcal M\nvDash _{\textsf {DM}}\neg \chi (c/v_{i})\). Thus \(\phantom {\dot {i}\!}\mathcal M\nvDash _{\textsf {DM}} \neg \,\exists v_{i}\chi \).
β‘
With Lemma 10 at hand one can check that all initial sequents in \(\phantom {\dot {i}\!}\mathcal S\) are satisfied by \(\phantom {\dot {i}\!}\mathcal M\).
This conclude the proof of Proposition 4. From the assumption \(\phantom {\dot {i}\!}\nvdash _{\mathcal S} \Gamma \Rightarrow \Delta \) we constructed (Ξ+,Ξ+) and the term model \(\phantom {\dot {i}\!}\mathcal M\). The reduct \(\phantom {\dot {i}\!}\mathcal M\restriction \mathcal {L}\) of \(\phantom {\dot {i}\!}\mathcal M\) to \(\phantom {\dot {i}\!}\mathcal {L}\) is such that \(\phantom {\dot {i}\!}\mathcal M\restriction \mathcal {L}\) is a model of \(\phantom {\dot {i}\!}\mathcal S\) and
for all ΟβΞ, \(\phantom {\dot {i}\!}\mathcal M\mathpunct \upharpoonright \mathcal L\vDash _{\textsf {DM}}\varphi \) and \(\phantom {\dot {i}\!} \mathcal M\mathpunct \upharpoonright \mathcal L\nvDash _{\textsf {DM}} \psi \) for all ΟβΞ.
Thus \(\phantom {\dot {i}\!}\Gamma \nvDash _{\mathcal S} \Delta \). This completes the proof of Proposition 4.
Rights and permissions
About this article
Cite this article
Halbach, V., Nicolai, C. On the Costs of Nonclassical Logic. J Philos Logic 47, 227β257 (2018). https://doi.org/10.1007/s10992-017-9424-3
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10992-017-9424-3