On the independence of premiss axiom and rule
- PDF / 397,220 Bytes
- 23 Pages / 439.37 x 666.142 pts Page_size
- 103 Downloads / 168 Views
Mathematical Logic
On the independence of premiss axiom and rule Hajime Ishihara1 · Takako Nemoto1 Received: 9 October 2018 / Accepted: 18 December 2019 © Springer-Verlag GmbH Germany, part of Springer Nature 2020
Abstract In this paper, we deal with a relationship among the law of excluded middle, the double negation elimination and the independence of premiss rule (IPR) for (many-sorted) intuitionistic predicate logic. After giving a general machinery, we give, as corollaries, several examples of extensions of HA and HAω which are closed under IPR but do not derive the independence of premiss axiom. Keywords Independence of premiss axiom · Independence of premiss rule · Non-classical axioms · Non-constructive axioms · Functional realizability interpretation Mathematics Subject Classification 03F50
1 Introduction It has been proved that intuitionistic first order arithmetic HA is closed under the independence of premiss rule (IPR) A → ∃x B ⇒ ∃x(A → B), (x not free in A, A Rasiowa−Harrop), for sentence A using, for example, Kleene or Aczel slash relation (cf. [9, Ch.3.5.16]). Troelstra [7, 3.7] showed that HAω is closed under the following IPRω in L (HAω ) A → ∃x σ B ⇒ ∃x σ (A → B), (x not free in A, A Rasiowa−Harrop),
B
Takako Nemoto [email protected] Hajime Ishihara [email protected]
1
School of Information Science, Japan Advanced Institute of Science and Technology, Nomi, Ishikawa 923-1292, Japan
123
H. Ishihara, T. Nemoto
for negative A using the modified realizability interpretation. In [2], we gave a class S of schemata such that HA+Λ and HAω +Λ are closed under IPR and IPRω whenever Λ is a subset of S . If an extension T of HA or HAω derives the independence of premiss axiom IP(ω) (A→∃x (σ ) B) → ∃x (σ ) (A→B), (x is not free in A, A Rasiowa–Harrop), then T is closed under IPR(ω) . Therefore a natural question arises: What theory T is closed under IPR(ω) , but does not derive IP(ω) ? In this paper, we give several examples of extensions of HA and HAω which are closed under IPR(ω) , but do not derive IP(ω) . In Sect. 2, we give a general relationship among the law of excluded middle (LEM), the double negation elimination (DNE) and IPR: if T Γ -LEM and T Γ -DNE, then T is not closed under IPR, and hence, in particular, T does not derive IP, for a class Γ of formulae and a theory T with a certain property. Using the relationship, we show that HA + Σn -LEM is closed under IPR but does not derive IP. In Sect. 3, we prove that several extensions of HAω with non-classical axiom schemata in S are closed under IPRω , but do not derive IPω . For that, we show that an extension S of them is consistent relative to an extension of EL, using two interpretations.
2 A general machinery and non-constructive principles 2.1 A general machinery We use the standard language of (many-sorted) first-order predicate logic containing ∧, ∨, →, ⊥, ∀ and ∃ as primitive logical operators. Prime formulae are atomic formulae or ⊥. Definition 1 We introduce certain predicate symbols ν 1 , ν 2 , ν 3 , . . .
Data Loading...
