A new version of Beth semantics for intuitionistic logic

1977 ◽  
Vol 42 (2) ◽  
pp. 306-308 ◽  
Author(s):  
Dov M. Gabbay
Keyword(s):  
Intuitionistic Logic ◽  
Predicate Logic ◽  
Tree Structure ◽  
Truth Conditions ◽  
Truth Definition ◽  
Image Position ◽  
Constant Domains ◽  
Condition B

We use the notation of Kripke's paper [1]. Let M = (G, K, R) be a tree structure and D a domain and η a Beth model on M. The truth conditions of the Beth semantics for ∨ and ∃ are (see [1]):(a) η (A ∨ B, H) = T iff for some B ⊆ K, B bars H and for each H′ ∈ B, either η(A, H′) = T or η(B, H′) = T.(b) η(∃xA(x), H) = T iff for some B ⊆ K, B bars H and for each H′ ∈ B there exists an a ∈ D such that η(A (a), H′) = T.Suppose we change the truth definition η to η* by replacing condition (b) by the condition (b*) (well known from the Kripke interpretation):Call this type of interpretation the new version of Beth semantics. We proveTheorem 1. Intuitionistic predicate logic is complete for the new version of the Beth semantics.Since Beth structures are of constant domains, and in the new version of Beth semantics the truth conditions for ∧, →, ∃, ∀, ¬ are the same as for the Kripke interpretation, we get:Corollary 2. The fragment without disjunction of the logic CD of constant domains (i.e. with the additional schema ∀x(A ∨ B(x))→ A ∨ ∀xB(x), x not free in A) equals the fragment without disjunction of intuitionistice logic.

Craig interpolation theorem for intuitionistic logic and extensions Part III

1977 ◽  
Vol 42 (2) ◽  
pp. 269-271 ◽  
Author(s):  
Dov M. Gabbay
Keyword(s):  
Possible Worlds ◽  
Predicate Logic ◽  
Interpolation Property ◽  
Interpolation Theorem ◽  
Kripke Structure ◽  
Unary Predicate ◽  
The World ◽  
Image Position ◽  
Constant Domains ◽  
Positive Integers

This is a continuation of two previous papers by the same title [2] and examines mainly the interpolation property for the logic CD with constant domains, i.e., the extension of the intuitionistic predicate logic with the schemaIt is known [3], [4] that this logic is complete for the class of all Kripke structures with constant domains.Theorem 47. The strong Robinson consistency theorem is not true for CD.Proof. Consider the following Kripke structure with constant domains. The set S of possible worlds is ω0, the set of positive integers. R is the natural ordering ≤. Let ω0 0 = , Bn, is a sequence of pairwise disjoint infinite sets. Let L0 be a language with the unary predicates P, P1 and consider the following extensions for P,P1 at the world m.(a) P is true on ⋃i≤2nBi, and P1 is true on ⋃i≤2n+1Bi for m = 2n.(b) P is true on ⋃i≤2nBi, and P1 for ⋃i≤2n+1Bi for m = 2n.Let (Δ,Θ) be the complete theory of this structure. Consider another unary predicate Q. Let L be the language with P, Q and let M be the language with P1, Q.

A logic stronger than intuitionism

1971 ◽  
Vol 36 (2) ◽  
pp. 249-261 ◽  
Author(s):  
Sabine Görnemann
Keyword(s):  
Intuitionistic Logic ◽  
Classical Logic ◽  
Predicate Logic ◽  
Predicate Calculus ◽  
Theoretical Methods ◽  
Axiom Scheme ◽  
Simple Notion ◽  
Image Position ◽  
Quasi Ordering

S. A. Kripke has given [6] a very simple notion of model for intuitionistic predicate logic. Kripke's models consist of a quasi-ordering (C, ≤) and a function ψ which assigns to every c ∈ C a model of classical logic such that, if c ≤ c′, ψ(c′) is greater or equal to ψ(c). Grzegorczyk [3] described a class of models which is still simpler: he takes, for every ψ(c), the same universe. Grzegorczyk's semantics is not adequate for intuitionistic logic, since the formulawhere х is not free in α. holds in his models but is not intuitionistically provable. It is a conjecture of D. Klemke that intuitionistic predicate calculus, strengthened by the axiom scheme (D), is correct and complete with respect to Grzegorczyk's semantics. This has been proved independently by D. Klemke [5] by a Henkinlike method and me; another proof has been given by D. Gabbay [1]. Our proof uses lattice-theoretical methods.

An intuitiomstic completeness theorem for intuitionistic predicate logic

1976 ◽  
Vol 41 (1) ◽  
pp. 159-166 ◽  
Author(s):  
Wim Veldman
Keyword(s):  
Intuitionistic Logic ◽  
Predicate Logic ◽  
Completeness Theorem ◽  
Point Of View ◽  
Foundations Of Mathematics ◽  
Strong Completeness ◽  
Recursive Predicate ◽  
Image Position ◽  
Primitive Recursive ◽  
Intuitionistic Mathematics

The problem of treating the semantics of intuitionistic logic within the framework of intuitionistic mathematics was first attacked by E. W. Beth [1]. However, the completeness theorem he thought to have obtained, was not true, as was shown in detail in a report by V. H. Dyson and G. Kreisel [2]. Some vague remarks of Beth's, for instance in his book, The foundations of mathematics, show that he sustained the hope of restoring his proof. But arguments by K. Gödel and G. Kreisel gave people the feeling that an intuitionistic completeness theorem would be impossible [3]. (A (strong) completeness theorem would implyfor any primitive recursive predicate A of natural numbers, and one has no reason to believe this for the usual intuitionistic interpretation.) Nevertheless, the following contains a correct intuitionistic completeness theorem for intuitionistic predicate logic. So the old arguments by Godel and Kreisel should not work for the proposed semantical construction of intuitionistic logic. They do not, indeed. The reason is, loosely speaking, that negation is treated positively.Although Beth's semantical construction for intuitionistic logic was not satisfying from an intuitionistic point of view, it proved to be useful for the development of classical semantics for intuitionistic logic. A related and essentially equivalent classical semantics for intuitionistic logic was found by S. Kripke [4].

scholarly journals On the correspondence between nested calculi and semantic systems for intuitionistic logics

2020 ◽  
Author(s):  
Tim Lyon
Keyword(s):  
Intuitionistic Logic ◽  
Structural Rules ◽  
First Order ◽  
Constant Domains ◽  
The Relationship ◽  
Intuitionistic Logics

Abstract This paper studies the relationship between labelled and nested calculi for propositional intuitionistic logic, first-order intuitionistic logic with non-constant domains and first-order intuitionistic logic with constant domains. It is shown that Fitting’s nested calculi naturally arise from their corresponding labelled calculi—for each of the aforementioned logics—via the elimination of structural rules in labelled derivations. The translational correspondence between the two types of systems is leveraged to show that the nested calculi inherit proof-theoretic properties from their associated labelled calculi, such as completeness, invertibility of rules and cut admissibility. Since labelled calculi are easily obtained via a logic’s semantics, the method presented in this paper can be seen as one whereby refined versions of labelled calculi (containing nested calculi as fragments) with favourable properties are derived directly from a logic’s semantics.

scholarly journals Some Remarks on a Recent Paper by Borch

1961 ◽  
Vol 1 (5) ◽  
pp. 265-272 ◽  
Author(s):  
Paul Markham Kahn
Keyword(s):  
Distribution Function ◽  
Random Variable ◽  
Fixed Number ◽  
Point Of View ◽  
Optimum Amount ◽  
Measurable Transformation ◽  
The Difference ◽  
Image Position ◽  
Stop Loss ◽  
Condition B

In his recent paper, “An Attempt to Determine the Optimum Amount of Stop Loss Reinsurance”, presented to the XVIth International Congress of Actuaries, Dr. Karl Borch considers the problem of minimizing the variance of the total claims borne by the ceding insurer. Adopting this variance as a measure of risk, he considers as the most efficient reinsurance scheme that one which serves to minimize this variance. If x represents the amount of total claims with distribution function F (x), he considers a reinsurance scheme as a transformation of F (x). Attacking his problem from a different point of view, we restate and prove it for a set of transformations apparently wider than that which he allows.The process of reinsurance substitutes for the amount of total claims x a transformed value Tx as the liability of the ceding insurer, and hence a reinsurance scheme may be described by the associated transformation T of the random variable x representing the amount of total claims, rather than by a transformation of its distribution as discussed by Borch. Let us define an admissible transformation as a Lebesgue-measurable transformation T such thatwhere c is a fixed number between o and m = E (x). Condition (a) implies that the insurer will never bear an amount greater than the actual total claims. In condition (b), c represents the reinsurance premium, assumed fixed, and is equal to the expected value of the difference between the total amount of claims x and the total retained amount of claims Tx borne by the insurer.

On Some Functional Equations of Carleman

1972 ◽  
Vol 15 (1) ◽  
pp. 129-131
Author(s):  
Charles G. Costley
Keyword(s):  
Scattering Theory ◽  
Functional Equations ◽  
Quantum Physics ◽  
Wave Equations ◽  
Hermitian Forms ◽  
Carleman Kernel ◽  
Linear Integral ◽  
Image Position ◽  
Linear Integral Equations ◽  
Condition B

The celebrated Fredholm theory of linear integral equations holds if the kernel K(x, y) or one of its iterates K(n) is bounded. Hilbert utilizing his theory of quadratic form was able to extend the theory to the kernels K(x, y) satisfyingabwhere k is independent of u(x).These theories were extended considerably by T. Carleman who deleted condition (b) above.Equations involving this Carleman kernel have been found useful in connection with Hermitian forms, continued fractions, Schroedinger wave equations (see [1], [2]) and more recently in scattering theory in quantum physics, etc. [3]. See also [5] for a variety of applications and extensions.

The decidability of the Kreisel-Putnam system

1970 ◽  
Vol 35 (3) ◽  
pp. 431-437 ◽  
Author(s):  
Dov M. Gabbay
Keyword(s):  
Intuitionistic Logic ◽  
Propositional Logic ◽  
Finite Model ◽  
Model Property ◽  
Intuitionistic Propositional Logic ◽  
Disjunction Property ◽  
Finite Model Property ◽  
Image Position

The intuitionistic propositional logic I has the following disjunction property This property does not characterize intuitionistic logic. For example Kreisel and Putnam [5] showed that the extension of I with the axiomhas the disjunction property. Another known system with this propery is due to Scott [5], and is obtained by adding to I the following axiom:In the present paper we shall prove, using methods originally introduced by Segerberg [10], that the Kreisel-Putnam logic is decidable. In fact we shall show that it has the finite model property, and since it is finitely axiomatizable, it is decidable by [4]. The decidability of Scott's system was proved by J. G. Anderson in his thesis in 1966.

On the formalisation of indirect discourse

1958 ◽  
Vol 23 (4) ◽  
pp. 417-419 ◽  
Author(s):  
R. L. Goodstein
Keyword(s):  
Predicate Logic ◽  
Logical Truth ◽  
Predicate Calculus ◽  
Inference Rules ◽  
First Order ◽  
Indirect Discourse ◽  
Image Position ◽  
Order Predicate Calculus

Mr. L. J. Cohen's interesting example of a logical truth of indirect discourse appears to be capable of a simple formalisation and proof in a variant of first order predicate calculus. His example has the form:If A says that anything which B says is false, and B says that something which A says is true, then something which A says is false and something which B says is true.Let ‘A says x’ be formalised by ‘A(x)’ and let assertions of truth and falsehood be formalised as in the following table.We treat both variables x and predicates A (x) as sentences and add to the familiar axioms and inference rules of predicate logic a rule permitting the inference of A(p) from (x)A(x), where p is a closed sentence.We have to prove that from

An improved prenex normal form1

1962 ◽  
Vol 27 (3) ◽  
pp. 317-326 ◽  
Author(s):  
C. C. Chang ◽  
H. Jerome Keisler
Keyword(s):  
Positive Integer ◽  
Predicate Logic ◽  
Atomic Formula ◽  
First Order ◽  
Empty String ◽  
Image Position ◽  
First Order Predicate Logic

Let ℒ be the set of all formulas of a given first order predicate logic (with or without identity). For each positive integer n, let ℒn be the set of all formulas φ in ℒ logically equivalent to a formula of the form where Q is a (possibly empty) string of quantifiers, m is a positive integer, and each αij is either an atomic formula or the negation of an atomic formula.

Sign in / Sign up

Export Citation Format

Share Document