Recently I’ve been working on axiomatizing a logic that results from adding a new operator to standard Intuitionistic Logic. I use $\sim$ for standard intuitionistic negation, and $\neg$ for the new “weak” negation operator. I have previously posted about this logic here Question about an extension of Intuitionistic Logic . In this post I use $\to$ for implication, while I’ve previously used $\implies$.
How should I go about proving completeness for this system? I am clear on proving soundness, but since there is more than one kind of negation, proving completeness is tricky. The semantics is somewhat complicated, so bear with me.
The semantics for NI is a Kripke-style semantics with a set of states W and a transitive and reflexive accessibility relation C between states. Each state has a domain D$_w$ which is the set of objects at state w. Further, there is a satisfaction relation ⊩ that evaluates whether or not a formula holds in a given model at a given state; there is a derivability relation ⊢ that evaluates syntactic consequence; finally, there is a semantic consequence relation ⊨. For the sake of simplicity, I define the semantics in terms of the classical “if and only if” (iff), but more complicated constructive definitions exist.
- w⊩¬φ iff there is a v s.t wCv and it is not the case that v⊩φ
- w⊩~φ iff for all v s.t. wCv it is not the case that v⊩φ
- w⊩φ iff for all v s.t. wCv v⊩φ is a positive literal
- w⊩φ→ψ iff for all v s.t. wCv, if v⊩φ then v⊩ψ
- w⊩φ∧ψ iff w⊩φ and w⊩ψ
- w⊩φ∨ψ iff w⊩φ or w⊩ψ
- w⊩ ∀$_0$xφ iff for all objects a∈D$_w$, w⊩φ(a)
- w⊩∀xφ iff for all objects a∈D$_v$ s.t. wCv, v⊩φ(a) (note that ∀ is a shorthand for ∀$_1$)
- w⊩∃xφ iff there is an object a∈D$_w$ s.t. w⊩φ(a)
- If Γ is a set of well-formed formulas (wffs), then Γ⊨ψ iff w,Γ⊩ψ for all states w in every model
Broadly speaking, there are two types of formulas, namely formulas that meet condition 1 and those that do not. The rules governing whether or not a formula meets condition 1 are as follows:
- Positive literals meet condition 1
- Wffs φ with main operator ~ meet condition 1.
- Implications meet condition 1.
- If a wff φ meets condition 1, then both ∀$_1$xφ and ∃xφ meet condition 1.
- If wffs φ and ψ meet condition 1, then (φ∨ψ) and (φ∧ψ) satisfy condition1.
- All and only condition 1 wffs are constructed with these rules.
The logical symbols of NI are {∧,∨,→,~,∀,∃,¬} with ~ being Intuitionistic negation, and ¬ as a kind of weak negation. The non-logical symbols of NI are brackets and English letters. Capital English letters are used for predicates, while lower-case letters f-h are used for functions. Other symbols may be added for more functions. Lower-case English letters a-e are used for constants, while i-t are used as propositional variables. Finally, u-z are used for first-order variables (variables). Numeral subscripts may be added to these non-logical symbols. A ‘term’ is a variable or a constant; predicates and functions range over both variables and constants. Commas are used to separate terms under the scope of a predicate or function. The only uses for brackets in NI is to separate binary connectives and to establish the range of a predicate or function. E.g., F(a), (p∧q), and g(x,y,z) are correct uses of brackets, while (~p), (q), and ((p→q)) are incorrect. Brackets may be dropped to avoid confusion in proofs and derivations. There are many different conventions for dropping brackets, so I leave such a choice open to the reader. The formation rules for constructing wffs are
- If φ is a propositional variable, φ is a wff.
- If φ is a predicate or a function with n terms, φ is a wff.
- If φ is a wff, then ~φ and ¬φ are wffs.
- A wff φ contains a free variable ‘x’ iff ∀0xφ and ∃xφ are wffs. Note that the state-specific universal quantifier ranges over every occurrence of the variable ‘x’ in φ.
- If ∃xφ is a wff and ‘x’ remains free in φ, then if ‘y’ is a variable free for ∃xφ, ∃y∃xφ[y/x] is a wff.
- A wff φ containing a free variable ‘x’ is either condition 1 or is a theorem iff ∀1xφ is a wff. Note that the universal quantifier ranges over every occurrence of the variable ‘x’ in φ.
- If φ and ψ are wffs, then (φ→ψ), (φ∧ψ), and (φ∨ψ) are wffs.
- All and only wffs are constructed with these rules.
Note that if φ does not meet condition 1 and φ is not a theorem, then these rules exclude ∀1xφ from being a wff. Also note that any positive literal is condition 1, such as propositional variables, functions, and predicates. This can be dropped for logics that are not preserving justification or proof.
Next I provide the axiom schemas and inference rules for Not-Intuitionistic Propositional Calculus (NIPC). The outermost brackets are dropped for clarity.
A1: (φ→(ψ→χ))→((φ→ψ)→(φ→χ))
A2: ~φ→(φ→ψ)
A3: (φ→~φ)→~φ
B1: φ→~¬φ condition 1 for φ
B2: ¬~¬φ→¬φ
B3: (φ→ψ)→(¬ψ→¬φ)
B4: (¬φ→φ)→(ψ→φ)
∨IL: φ→(φ∨ψ)
∨IR: ψ→(φ∨ψ)
∨E: ((φ∧ψ)→χ)→(((φ∧π)→χ)→((φ∧(ψ∨π))→χ))
∧EL: (φ∧ψ)→φ
∧ER: (φ∧ψ)→ψ
∧I: (φ→ψ)→((φ→χ)→(φ→(φ∧(ψ∧χ))))
K: ∀$_{i≤1}$x(φ∨ψ)→(φ∨∀$_0$xψ) where x is not free in φ
DIST: ∀x(φ→ψ)→(φ→∀$_{i}$xψ) where x is not free in φ; note that i=0 if either φ or ψ do not meet condition 1; i=1 otherwise
∀E: ∀$_{i≤1}$xφ(x)→φ(t)[x/t] for any term t at any state v such that t∈Dv
∃E: ∀x((φ∧χ)→ψ)→((∃xφ∧χ)→ψ) x free in neither ψ nor χ
∃I: φ(t)→∃xφ(x)[x/t] for any term t at any state v such that t∈Dv
=I: t=t for any term t
=E: From (t$_1$=t$_2$) and φ(t$_1$), infer φ(t$_2$) for any terms t$_1$,t$_2$
MP:From φ and (φ→ψ), infer ψ
∀I: From φ, infer ∀$_1$xφ