An aPempt at disentangling logical and semanQcal necessity

A justification of Necessitation A short recap of semantics for intuitionism versus modal Some preliminary results In a possible future world An attempt at disentangling logical and semantical necessity Second Workshop on Worlds and Truth Values, Barcelona Iris van der Giessen, Joost J. Joosten, Paul Mayaux, Vicent Navarro Arroyo University of Barcelona Tuesday 11-06-2024 I vd Giessen, J. J. Joosten, P. Mayaux, V. Navarro On Necessity/Contingency of Logic 1 / 25 A justification of Necessitation A short recap of semantics for intuitionism versus modal Some preliminary results In a possible future world Necessitation and Logic A framework to study the Contingency of Logic Semantic justification ▶ If |= A stands for A is true at any possible world. ▶ and, if the semantics of ✷A is stipulated by ✷A is true at some possible world w if and only if A is true at all possible worlds of w . ▶ Then the Necessitation rule I vd Giessen, J. J. Joosten, P. Mayaux, V. Navarro A ✷A has a clear justification. On Necessity/Contingency of Logic 2 / 25 A justification of Necessitation A short recap of semantics for intuitionism versus modal Some preliminary results In a possible future world Necessitation and Logic A framework to study the Contingency of Logic A common misconception ▶ The rule of Necessitation If I know that A, then, I may conclude that ✷A. ▶ Wrong application of Necessitation: [ϕ]1 . ✷ϕ Nec ϕ → ✷ϕ →I, 1 I vd Giessen, J. J. Joosten, P. Mayaux, V. Navarro On Necessity/Contingency of Logic 3 / 25 A justification of Necessitation A short recap of semantics for intuitionism versus modal Some preliminary results In a possible future world Necessitation and Logic A framework to study the Contingency of Logic Epistemic justification of Necessity ▶ How to interpret modal reasoning ⊢ ▶ If ⊢ is just an artifact to model |= then as before, Necessitation is clear ▶ If we try to endow ⊢ with an independent epistemic justification for reasoning about Necessity, then ▶ the Rule of Necessity seems to impose some Necessary status of reasoning/logic: If I can justify the validity of A using my reasoning system then since this reasoning is necessary necessarily A is also justified for my reasoning system ▶ The conclusion seems to be: logic is necessary ▶ However, the possible world semantics allows for different possible worlds ruled by different logics I vd Giessen, J. J. Joosten, P. Mayaux, V. Navarro On Necessity/Contingency of Logic 4 / 25 A justification of Necessitation A short recap of semantics for intuitionism versus modal Some preliminary results In a possible future world Necessitation and Logic A framework to study the Contingency of Logic Defining the Language and Derivations ▶ Language L□ := p | ⊥ | A ∧ A | A ∨ A | A → A | □A ▶ Set Form□ of formulas in L□ ▶ (Γ, ϕ ⊆ Form□ ) A classical derivation D from Γ to ϕ is a sequence of formulas ϕ1 , ϕ2 , ..., ϕk s.t ∀i ∈ {1, 2, ..., k}: ▶ ▶ ▶ ▶ ϕi ∈ Γ or ϕi is in the form of a Classical tautology in the language L□ or There is j, l < i such that ϕj is of the form ϕl → ϕi ϕk = ϕ. I vd Giessen, J. J. Joosten, P. Mayaux, V. Navarro On Necessity/Contingency of Logic 5 / 25 A justification of Necessitation A short recap of semantics for intuitionism versus modal Some preliminary results In a possible future world Necessitation and Logic A framework to study the Contingency of Logic Defining the Language and Derivations ▶ (Γ, ϕ ⊆ Form□ ) An Intuitionistic derivation D from Γ to ϕ is a sequence of formulas ϕ1 , ϕ2 , ..., ϕk s.t ∀i ∈ {1, 2, ..., k}: ▶ ϕi ∈ Γ or ▶ ϕi is in the form of an Intuitionistic tautology in the language L□ or ▶ There is j, l < i such that ϕj is of the form ϕl → ϕi ▶ ϕk = ϕ. L□ □ ▶ ⊢L represents a classical/intuitionistic derivation in L□ c / ⊢i L□ □ ▶ Tc□ /Ti□ is the closure of T over ⊢L c / ⊢i I vd Giessen, J. J. Joosten, P. Mayaux, V. Navarro On Necessity/Contingency of Logic 6 / 25 A justification of Necessitation A short recap of semantics for intuitionism versus modal Some preliminary results In a possible future world Necessitation and Logic A framework to study the Contingency of Logic Defining the models ▶ A Mixed model is a tuple M := ⟨W , R, e⟩ where ⟨W , R⟩ is a Kripke Frame and e is an extension
e : W → P(Form□ ) × {i, c} denoted e(w ) = ⟨Tw , lw ⟩ such that: 1. 2. 3. 4. ⊥∈ / Tw ; L T w ⊢l w □ ϕ ⇒ ϕ ∈ T w ; □ϕ ∈ Tw ⇐⇒ ∀v (wRv ⇒ ϕ ∈ Tw ); ¬□ϕ ∈ Tw ⇐⇒ ∃u(wRu ∧ ϕ ∈ / Tu ). I vd Giessen, J. J. Joosten, P. Mayaux, V. Navarro On Necessity/Contingency of Logic 7 / 25 A justification of Necessitation A short recap of semantics for intuitionism versus modal Some preliminary results In a possible future world Necessitation and Logic A framework to study the Contingency of Logic First examples of Mixed Models ▶ w1 (c) w2 (i) i ▶ Fw2 = {p, q} ∪ {□ϕ | ϕ ∈ Form□ } □ ; c ▶ Fw1 = {¬q} ∪ {□ϕ | ϕ ∈ Fw2 } ∪ {¬□ψ | ψ ∈ Form□ /Fw2 } □ w2 (i) w1 (c) w3 (c) ▶ c ▶ Fw3 = {p} ∪ {□ϕ | ϕ ∈ Form□ } □ i ▶ Fw2 = {p, q} ∪ {□ϕ | ϕ ∈ Form□ } □ ▶ Fw1 = c□ {¬p ∨ q} ∪ {□ϕ | ϕ ∈ Fw2 ∩ Fw3 } ∪ {¬□ψ | ψ ∈ Form□ /Fw2 ∩ Fw3 } I vd Giessen, J. J. Joosten, P. Mayaux, V. Navarro On Necessity/Contingency of Logic 8 / 25 A justification of Necessitation A short recap of semantics for intuitionism versus modal Some preliminary results In a possible future world Basic Kripke semantics Bi-Relational models Intuitionistic logic and Modal logic ▶ Intuitionistic propositional logic IPC: ▶ Language: A ::= p | ⊥ | A ∧ A | A ∨ A | A → A ▶ Intuitionistic tautologies ▶ Rules: Modus Ponens ▶ Classical modal logic K: ▶ ▶ ▶ ▶ Language: A ::= p | ⊥ | A ∧ A | A ∨ A | A → A | ✷A| ✸A Classical tautologies K-axiom: ✷(A → B) → ✷A → ✷B Rules: Modus Ponens and Necessitation I vd Giessen, J. J. Joosten, P. Mayaux, V. Navarro On Necessity/Contingency of Logic 9 / 25 A justification of Necessitation A short recap of semantics for intuitionism versus modal Some preliminary results In a possible future world Basic Kripke semantics Bi-Relational models Intuitionistic logic and Modal logic: Semantics ▶ Kripke semantics for IPC: ▶ M = (W , ≤, V ) (Monotonicity w.r.t. V ) ▶ M, w ⊩ A → B iff for all v ≥w : M, v ⊩ A implies M, v ⊩ B ▶ Possible world semantics for K: ▶ M = (W , R, V ) ▶ M, w ⊩ ✷A iff for all v s.t. w Rv : M, v ⊩ A M, w ⊩ ✸A iff there exists v s.t. w Rv and M, v ⊩ A I vd Giessen, J. J. Joosten, P. Mayaux, V. Navarro On Necessity/Contingency of Logic 10 / 25 A justification of Necessitation A short recap of semantics for intuitionism versus modal Some preliminary results In a possible future world Basic Kripke semantics Bi-Relational models Some examples p, q p q p, q q q w w ⊩p→q I vd Giessen, J. J. Joosten, P. Mayaux, V. Navarro p, q w w ⊮ ◻◻q w ⊩ ◇◇q w ⊩ ◻◻p On Necessity/Contingency of Logic 11 / 25 A justification of Necessitation A short recap of semantics for intuitionism versus modal Some preliminary results In a possible future world Basic Kripke semantics Bi-Relational models Intuitionistic modal logics Quest to intuitionistic meaning of ✷ and ✸ Classical consequences of the K-axiom: (k1) (k2) (k3) (k4) (k5) ✷(A → B) → ✷A → ✷B ✷(A → B) → ✸A → ✸B ✸(A ∨ B) → ✸A ∨ ✸B (✸A → ✷B) → ✷(A → B) ¬✸⊥ Different intuitionistic/constructive modal logics: ▶ iK := IPC + (k1) ▶ CK := IPC + (k1) + (k2) ▶ IK := IPC + (k1) + (k2) + (k3) + (k4) + (k5) ▶ ... I vd Giessen, J. J. Joosten, P. Mayaux, V. Navarro On Necessity/Contingency of Logic 12 / 25 A justification of Necessitation A short recap of semantics for intuitionism versus modal Some preliminary results In a possible future world Basic Kripke semantics Bi-Relational models Intermezzo Theorem iK and CK prove the same ✸-free theorems Theorem (Das&Marin, 2023) iK and IK do not have the same ✸-free theorems For example: ¬¬✷⊥ → ✷⊥ ∈ IK \ iK ¬¬✷p → ✷p ∈ IK \ iK I vd Giessen, J. J. Joosten, P. Mayaux, V. Navarro On Necessity/Contingency of Logic 13 / 25 A justification of Necessitation A short recap of semantics for intuitionism versus modal Some preliminary results In a possible future world Basic Kripke semantics Bi-Relational models Birelational semantics for iK ▶ M = (W , ≤, R, V ) (Monotonicity w.r.t. V ) ▶ Frame property (F0): y z x ▶ M, w ⊩ ✷A iff for all v s.t. w Rv : M, v ⊩ A I vd Giessen, J. J. Joosten, P. Mayaux, V. Navarro On Necessity/Contingency of Logic 14 / 25 A justification of Necessitation A short recap of semantics for intuitionism versus modal Some preliminary results In a possible future world Basic Kripke semantics Bi-Relational models Birelational semantics for IK ▶ M = (W , ≤, R, V ) (Monotonicity w.r.t. V ) ▶ Frame properties (F1) and (F2): y ∃v ∃v z x z x y ▶ M, w ⊩ ✷A iff for all w ′ ≥w and all v s.t. w ′ Rv : M, v ⊩ A M, w ⊩ ✸A iff there exists v s.t. w Rv and M, v ⊩ A I vd Giessen, J. J. Joosten, P. Mayaux, V. Navarro On Necessity/Contingency of Logic 15 / 25 A justification of Necessitation A short recap of semantics for intuitionism versus modal Some preliminary results In a possible future world Concrete models Soundness On Completeness Concrete models ▶ Concrete Models: From a KF F = ⟨W , R⟩ and function λ : W → {c, i}, we assign to each w ∈ W a rooted intuitionistic Kripke Model ⟨Uw , ≤w , Vw ⟩(root: w ∈ Uw ) st λ(w ) = c ⇒ Uw = {w } S ▶ ⊩ is defined on Θ := Uw (for x ∈ Uw ): w ∈W 1. 2. 3. 4. 5. 6. 7. x x x x x x x ⊩ ⊥ and x ⊩ ⊤; ⊩ p iff x ∈ Vw (p); ⊩ A ∧ B iff x ⊩ A and x ⊩ B; ⊩ A ∨ B iff x ⊩ A or x ⊩ B; ⊩ A → B iff ∀y ∈ Uw (x ≤ y → y ⊩ A or y ⊩ B); ⊩ ¬A iff x ⊩ A → ⊥; ⊩ ✷A iff ∀v (wRv → v ⊩ A). I vd Giessen, J. J. Joosten, P. Mayaux, V. Navarro On Necessity/Contingency of Logic 16 / 25 A justification of Necessitation A short recap of semantics for intuitionism versus modal Some preliminary results In a possible future world Concrete models Soundness On Completeness Predicate models for IK ▶ iK embeds into K via the Kuroda translation, ▶ IK embeds into K via the Gödel-Gentzen translation, moreover, ▶ IK embeds into IQC by the standard translation: ST (A) := ∀xSTx (A) with STx (✷A) := ∀y (xRy → STy (A)) STx (✸A) := ∃y (xRy ∧ STy (A)) ▶ Predicate models ⇒ birelational semantics with (F1) and (F2) I vd Giessen, J. J. Joosten, P. Mayaux, V. Navarro On Necessity/Contingency of Logic 17 / 25 A justification of Necessitation A short recap of semantics for intuitionism versus modal Some preliminary results In a possible future world Concrete models Soundness On Completeness Predicate models for IK We observe that Concrete Mix Models are dual to predicate models of IK! Dv Du Dw M, w ⊩ ∀xϕ iff for all w ′ ≥w and all d ∈ Dw ′ : M, w ′ ⊩ ϕ[x/d] M, w ⊩ ∃xϕ iff there exists d ∈ Dw s.t. M, w ⊩ ϕ[x/d] I vd Giessen, J. J. Joosten, P. Mayaux, V. Navarro On Necessity/Contingency of Logic 18 / 25 A justification of Necessitation A short recap of semantics for intuitionism versus modal Some preliminary results In a possible future world Concrete models Soundness On Completeness Conjecture for Concrete models ▶ Theorem: Let Γw := {ϕ | w ⊩ ϕ}. The KF F together with the extention e defined e(w ) = ⟨Γw ; λ(w )⟩ defines a Mixed Model, called Concrete Model. ▶ Example of a non-concrete Mixed Model: F = ⟨{w }, R⟩, c R = ∅, lw = c, Tw = {p ∨ q} ∪ {□ϕ | ϕ ∈ Form□ } ▶ Conjecture: The class CM of all Concrete Models is the class of all Mixed Models such that for all M ∈ CM, w ∈ M: ▶ If lw = c, Tw is a maximal theory ▶ If lw = i, Tw is a prime theory (ϕ ∨ ψ ∈ Tw ⇒ ϕ ∈ Tw or ψ ∈ Tw ). I vd Giessen, J. J. Joosten, P. Mayaux, V. Navarro On Necessity/Contingency of Logic 19 / 25 A justification of Necessitation A short recap of semantics for intuitionism versus modal Some preliminary results In a possible future world Concrete models Soundness On Completeness Soundness for MM ▶ Soundness: iK + ✷A ∨ ¬✷A is sound with respect to the class MM of all Mixed Models. ▶ Results of interest: ▶ (Necessitation)M ⊨ A implies M ⊨ □A; ▶ (Distributivity)M ⊨ □(A → B) → (□A → □B). I vd Giessen, J. J. Joosten, P. Mayaux, V. Navarro On Necessity/Contingency of Logic 20 / 25 A justification of Necessitation A short recap of semantics for intuitionism versus modal Some preliminary results In a possible future world Concrete models Soundness On Completeness Quick proof of Distributivity(k-axiom) ▶ (M ∈ MM) We want M ⊨ □(A → B) → (□A → □B) (i.e ∀w ∈ M, □(A → B) → (□A → □B) ∈ Tw ) ▶ (A □(A → B) ∈ Fw ) ▶ If □A ∈ Fw , ∀y ∈ M(A, A → B ∈ Fy ⇒ B ∈ Fy ) ⇒ □B ∈ Fw ⇒ □(A → B) → (□A → □B) ▶ If □A ∈ / Fw , □A → ⊥ ∈ Fw , and by reductio ad absurdum, □A → □B ∈ Fw ⇒ □(A → B) → (□A → □B) ∈ Tw ▶ ((A □(A → B) ∈ / Fw ), then □(A → B) → ⊥ ∈ Fw and by reductio ad absurdum, □(A → B) → (□A → □B) ∈ Tw I vd Giessen, J. J. Joosten, P. Mayaux, V. Navarro On Necessity/Contingency of Logic 21 / 25 A justification of Necessitation A short recap of semantics for intuitionism versus modal Some preliminary results In a possible future world Concrete models Soundness On Completeness Frame condition and possible completeness ▶ Frame condition for □A ∨ ¬□A (F3): y z x ▶ Completeness of MM with regards to iK+□A ∨ ¬□A Would require: ▶ Completeness of Birelational models BM with (F0+F3) with regards to iK+□A ∨ ¬□A ▶ Transition from BM to MM Models (Unraveling) I vd Giessen, J. J. Joosten, P. Mayaux, V. Navarro On Necessity/Contingency of Logic 22 / 25 A justification of Necessitation A short recap of semantics for intuitionism versus modal Some preliminary results In a possible future world Other logics Temporal logics Combining various logics ▶ Incomparable, for example ▶ Gödel-Dummett logic LC of linear Kripke frames (p → q) ∨ (q → p) ▶ Intuitionistic Logic of bounded depth two BD2 p ∨ (p → (q ∨ ¬q)) ▶ Many valued ▶ Etc. I vd Giessen, J. J. Joosten, P. Mayaux, V. Navarro On Necessity/Contingency of Logic 23 / 25 A justification of Necessitation A short recap of semantics for intuitionism versus modal Some preliminary results In a possible future world Other logics Temporal logics On the structure of time ▶ Locally, time can behave differently than globally ▶ Universal time versus black-hole horizon, etc. ▶ combining different temporal logics I vd Giessen, J. J. Joosten, P. Mayaux, V. Navarro On Necessity/Contingency of Logic 24 / 25 A justification of Necessitation A short recap of semantics for intuitionism versus modal Some preliminary results In a possible future world Other logics Temporal logics Thank you for your attention and feedback I vd Giessen, J. J. Joosten, P. Mayaux, V. Navarro On Necessity/Contingency of Logic 25 / 25