Abstract
Free logics is a family of first-order logics which came about as a result of examining the existence assumptions of classical logic. What those assumptions are varies, but the central ones are that (i) the domain of interpretation is not empty, (ii) every name denotes exactly one object in the domain and (iii) the quantifiers have existential import. Free logics usually reject the claim that names need to denote in (ii), and of the systems considered in this paper, the positive free logic concedes that some atomic formulas containing non-denoting names (namely self-identity) are true, while negative free logic rejects even the latter claim. Inclusive logics, which reject (i), are likewise considered. These logics have complex and varied axiomatizations and semantics, and the goal of this paper is to present an orderly examination of the various systems and their mutual relations. This is done by first offering a formalization, using sequent calculi which possess all the desired structural properties of a good proof system, including admissibility of contraction and cut, while streamlining free logics in a way no other approach has. We then present a simple and unified system of abstract semantics, which allows for a straightforward demonstration of the meta-theoretical properties, and offers insights into the relationship between different logics (free and classical). The final part of this paper is dedicated to extending the system with modalities by using a labeled sequent calculus, and here we are again able to map out the different approaches and their mutual relations using the same framework.
Article PDF
Similar content being viewed by others
References
Antonelli, G. (2000). Proto-Semantics for positive free logic. Journal of Philosophical Logic, 29, 277–294.
Bencivenga, E. (2002). Free logics. In Gabbay, D., & Guenthner, F. (Eds.) Handbook of philosophical logic, (Vol. 5 pp. 147–196). Dordrecht: Springer.
Berry, G.D.W. (1941). On Quine’s axioms of quantification. The Journal of Symbolic Logic, 6, 23–27.
Feferman, S. (1995). Definedness. Erkenntnis, 43, 295–320.
Garson, J. (1991). Applications of free logic to quantified intensional logic. In Lambert, K. (Ed.) Philosophical applications of free logic, (Vol. 5 pp. 111–142). New York: Oxford University Press.
Gratzl, N. (2010). A sequent calculus for a negative free logic. Studia Logica, 96, 331– 348.
Hailperin, T. (1953). Quantification theory and empty individual domains. The Journal of Symbolic Logic, 18, 197–200.
Hintikka, J. (1959). Existential presuppositions and existential commitments. The Journal of Philosophy, 56, 125–137.
Lambert, K. (1967). Free logic and the concept of existence. Notre Dame Journal of Formal Logic, 8, 133–144.
Lambert, K. (1997). Free logics: their foundations, character, and some applications thereof. Sankt Augustin: Academia Verlag.
Lambert, K. (2001). Free logics. In Goble, L. (Ed.) The Blackwell guide to philosophical logic (pp. 258–279). Malden, Oxford, Carlton, Berlin: Blackwell Publishers.
Lehmann, S. (2002). More free logics. In Gabbay, D., & Guenthner, F. (Eds.) Handbook of philosophical logic, (Vol. 5 pp. 197–259). Dordrecht: Springer.
Leitgeb, H. (2019). HYPE: A system of hyperintensional logic (with an application to semantic paradoxes). Journal of Philosophical Logic, 48, 305–405.
Maffezioli, P., & Orlandelli, E. (2019). Full cut elimination and interpolation for intuitionistic logic with existence predicate. Bulletin of the Section of Logic, 48(2), 137–158.
Morscher, E., & Hieke, A. (2013). New essays in free logic: In honour of Karel Lambert. Dordrecht: Springer.
Negri, S. (2005). Proof analysis in modal logic. Journal of Philosophical Logic, 34, 507–544.
Negri, S., & Orlandelli, E. (2019). Proof theory for quantified monotone modal logics. Logic Journal of the IGPL, 27, 478–506.
Negri, S., & von Plato, J. (1998). Cut elimination in the presence of axioms. The Bulletin of Symbolic Logic, 4, 418–435.
Negri, S., & von Plato, J. (2001). Structural proof theory. Cambridge: Cambridge University Press.
Negri, S., & von Plato, J. (2011). Proof analysis: A contribution to Hilbert’s last problem. Cambridge: Cambridge University Press.
Nolt, J. (2018). Free Logic. In Zalta, E.N. (Ed.) The Stanford Encyclopedia of Philosophy (Fall 2018 Edition) https://plato.stanford.edu/archives/fall2018/entries/logic-free/. Accessed 13 December 2019.
Pavlović, E., & Gratzl, N. (2019). Proof-Theoretic analysis of the Quantified argument calculus. The Review of Symbolic Logic, 12(4), 607–636.
Quine, W.V. (1954). Quantification and the empty domain. The Journal of Symbolic Logic, 19, 177–179.
Troelstra, A., & Schwichtenberg, H. (2000). Basic proof theory. Cambridge: Cambridge University Press.
Funding
Open access funding provided by University of Helsinki including Helsinki University Central Hospital. This paper was written with support of the Academy of Finland research project no. 1308664. This paper was written with support of the Deutsche Forschungsgemeinschaft (DFG) research project no. 390218268
Author information
Authors and Affiliations
Corresponding author
Additional information
Publisher’s Note
Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.
An anonymous reviewer has offered numerous suggestions which have, combined, amounted to a significant improvement of the paper, and for that we extend our gratitude. Special thanks goes to O. Foisch.
Appendices
Appendix A: Structural properties
Lemma 2.4 (α-conversion)
A derivation (where ⊩n denotes derivability with height bounded by n) of ⊩nΓ ⇒Δ can be converted into a derivation of \(\vdash _{n}{\Gamma }^{\prime } \Rightarrow {\Delta }^{\prime }\), where \({\Gamma }^{\prime }\) and \({\Delta }^{\prime }\) differ from Γ and Δ, respectively, only in namings of bound variables.
Proof
By induction on the height of a derivation.
If Γ ⇒Δ is an initial sequent, then so is \({\Gamma }^{\prime } \Rightarrow {\Delta }^{\prime }\). If the last rule is any of the propositional or identity rules, the namings remain unchanged from the premis(es). If the last rule applied is R∀, then it is derived from some sequent E!t,Γ ⇒Δ,A[t/x]. By the inductive hypothesis \( E! t, {\Gamma }^{\prime } \Rightarrow {\Delta }^{\prime }, A [y/x][t/y] \) is likewise derivable, so by applying R∀ we obtain \( {\Gamma }^{\prime } \Rightarrow {\Delta }^{\prime }, \forall y A [y/x] \). Similar for other quantifier rules and simple for the rule E!. □
Lemma 2.5 (Substitution)
If ⊩nΓ ⇒Δ is derivable in G3pf (G3nf), then ⊩nΓ[t/s] ⇒Δ[t/s] is derivable.
Proof
By induction on the height of the derivation. If Γ ⇒Δ is an initial sequent, then so is Γ[t/s] ⇒Δ[t/s].
Propositional rules do not alter the free and bound individual variables between their premis(es) and conclusion. The rules =Ref and E! in G3nf also do not alter the free and bound individual variables between their premise and conclusion, and the step is straightforward for =Ref in G3pf. The rule =Repl does not alter the free and bound individual variables.
If the last rule applied is R∀ and t is an eigenvariable of that application of the rule (otherwise we skip the first application of the inductive hypothesis), the premise of the application of the rule is some E!t,Γ ⇒Δ,A[t/x]. We use the inductive hypothesis to replace it with some d that has not so far occurred anywhere above that application of the rule to obtain E!d,Γ ⇒Δ,A[t/x][d/t] (we know by eigenvariable condition that t does not occur in Γ or Δ), which is the same as E!d,Γ ⇒Δ,A[d/x]. Using the inductive hypothesis again we get E!d,Γ[t/s] ⇒Δ[t/s],A[d/x][t/s], which is the same as E!d,Γ[t/s] ⇒Δ[t/s],A[t/s][d/x]. Now we apply R∀ to obtain Γ[t/s] ⇒Δ[t/s],∀xA[t/s]. Similar for other quantifier rules. □
Lemma 2.6 (Axiom generalization)
Any sequent of the form A,Γ ⇒Δ,A is derivable in G3pf and G3nf.
Proof
By induction on the weight of A. Since the two systems do not differ in their language, the proofs proceed the same. The interesting cases here are for quantified formulas:
□
Lemma 2.7 (Weakening)
Weakening is height-preserving admissible in G3pf and G3nf:
-
i)
If ⊩nΓ ⇒Δ then ⊩nC,Γ ⇒Δ.
-
ii)
If ⊩nΓ ⇒Δ then ⊩nΓ ⇒Δ,C.
Proof
Routine by induction on the height of the derivation, using Lemma 2.5 when necessary. □
Lemma 2.8 (Invertibility)
All the rules of G3pf and G3nf are height-preserving invertible.
Proof
Straightforward for propositional rules, follows from Lemma 2.7 for all other rules except R∀ and L∃. So what remains to be shown is:
-
i)
If ⊩nΓ ⇒Δ,∀xA, then ⊩nE!t,Γ ⇒Δ,A[t/x], and
-
ii)
if ⊩n∃xA,Γ ⇒Δ, then ⊩nE!t, A[t/x],Γ ⇒Δ.
We demonstrate (i) by induction on the height of the derivation, n.
If n = 0, then Γ ⇒Δ,∀xA is an initial sequent, but then so is E!t,Γ ⇒Δ,A[t/x].
If n > 0, then if ∀xA is not principal in the last step, Γ ⇒Δ,∀xA follows from some sequents \(E! t,{\Gamma }^{\prime } \Rightarrow {\Delta }^{\prime }, \forall x A\) (\(E! t,{\Gamma }^{\prime \prime } \Rightarrow {\Delta }^{\prime \prime }, \forall x A\)) with height ≤ n − 1. Applying the Lemma 2.5 if t is an eigenvariable of the application of the rule and then the inductive hypothesis, we obtain \(E! t,{\Gamma }^{\prime } \Rightarrow {\Delta }^{\prime }, A[t/x]\) (\(E! t,{\Gamma }^{\prime \prime } \Rightarrow {\Delta }^{\prime \prime }, A[t/x]\)), and then applying the rule again we get E!t,Γ ⇒Δ,A[t/x].
If on the other hand ∀xA is principal, then the upper sequent of the last application of the rule is already of the required form and with height ≤ n.
Parallel for (ii). □
Lemma 2.9 (Contraction)
Contraction is height-preserving admissible in G3pf and G3nf:
-
i)
If ⊩nC, C,Γ ⇒Δ then ⊩nC,Γ ⇒Δ.
-
ii)
If ⊩nΓ ⇒Δ,C, C then ⊩nΓ ⇒Δ,C.
Proof
Simultaneous for (i) and (ii) by induction on the height of the derivation. The interesting part is when the formula C is principal in R∀ or L∃.
So, assume that C is ∀xA and principal in R∀ in the last step. Then the last step of the derivation is Γ ⇒Δ,∀xA,∀xA, derived by R∀ from E!t,Γ ⇒Δ,∀xA, A[t/x]. Applying the Lemma 2.8 to that sequent we get E!t, E!t,Γ ⇒Δ,A[t/x],A[t/x] with the same height of ≤ n − 1. We then apply the inductive hypothesis to obtain E!t,Γ ⇒Δ,A[t/x] and then R∀ to finally obtain Γ ⇒Δ,∀xA. Similar for L∃. □
Theorem 2.10
Cut is admissible in G3pf and G3nf.
Proof
By induction on the weight of a formula and subinduction on the sum of heights of the two upper sequents of a cut. Standard for propositional rules, identity rules in G3pf and the rule =Repl in G3nf. We check the remaining cases.
When the cut formula is principal in the rule E! the cut has the following form:
If Γ1 ⇒Δ1,P[t] is an initial sequent we distinguish two cases. First, if Γ1 ⇒Δ1,P[t] is of the form \(P[t], {\Gamma }_{1}^{\prime }\Rightarrow {\Delta }_{1}, P[t]\) (i.e. if Γ1 contains P[t]), then the bottom sequent of the cut is of the form \(P[t], {\Gamma }_{1}^{\prime },{\Gamma }_{2}\Rightarrow {\Delta }_{1}, {\Delta }_{2}\) and can be obtained from P[t],Γ2 ⇒Δ2 using Lemma 2.7. Second, if Γ1 does not contain P[t], then Γ1 ⇒Δ1 is likewise an initial sequent.
If Γ1 ⇒Δ1,P[t] is not initial then the derivation has the following form (since an atomic formula cannot be principal on the right):
This is transformed into:
Here cuts numbered (1) and (2) are of lesser height. Similar for the rule =Ref of G3nf.
When the cut formulas are quantified the interesting case is when they are principal in both upper sequents. In the case of ∀, the cut is then of the form:
This is transformed into:
Here the cut numbered (1) is of lesser weight and (2) are of lesser height. Similar for ∃. □
Appendix B: Adequacy of axioms
Theorem 2.16
All of the PFL axioms A1-A6 are derivable in G3pf.
Proof
-
A1:
∀x(A → B) → (∀xA →∀xB)
-
A2:
A →∀xA
-
A3:
∀xA → (E!t → A[t/x])
-
A4:
∀xE!x
-
A5:
s = t → (A → A[t//s])
-
A6:
t = t
□
Theorem 2.17
All of the NFL axioms A1-A7 are derivable in G3nf.
Proof
Since most of the axioms are the same in both systems, it only remains to show that the different version of A6, and the new axiom A7, are derivable.
-
A6:
∀x(x = x)
-
A7:
Pt1,…,tn → E!ti, 1 ≤ i ≤ n
□
Rights and permissions
Open Access This article is licensed under a Creative Commons Attribution 4.0 International License, which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons licence, and indicate if changes were made. The images or other third party material in this article are included in the article's Creative Commons licence, unless indicated otherwise in a credit line to the material. If material is not included in the article's Creative Commons licence and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder. To view a copy of this licence, visit http://creativecommons.org/licenses/by/4.0/.
About this article
Cite this article
Pavlović, E., Gratzl, N. A More Unified Approach to Free Logics. J Philos Logic 50, 117–148 (2021). https://doi.org/10.1007/s10992-020-09564-7
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10992-020-09564-7