scholarly journals Fixed-point Elimination in the Intuitionistic Propositional Calculus

2020 ◽  
Vol 21 (1) ◽  
pp. 1-37 ◽  
Author(s):  
Silvio Ghilardi ◽  
Maria João Gouveia ◽  
Luigi Santocanale
Keyword(s):  
Fixed Point ◽  
Propositional Calculus ◽  
Intuitionistic Propositional Calculus

scholarly journals On an interpretation of second order quantification in first order intuitionistic propositional logic

1992 ◽  
Vol 57 (1) ◽  
pp. 33-52 ◽  
Author(s):  
Andrew M. Pitts
Keyword(s):  
Propositional Logic ◽  
Heyting Algebra ◽  
Propositional Calculus ◽  
Interpolation Theorem ◽  
Second Order ◽  
Heyting Algebras ◽  
Intuitionistic Propositional Logic ◽  
First Order ◽  
Intuitionistic Propositional Calculus ◽  
Algebraic Counterpart

AbstractWe prove the following surprising property of Heyting's intuitionistic propositional calculus, IpC. Consider the collection of formulas, ϕ, built up from propositional variables (p, q, r, …) and falsity (⊥) using conjunction (∧), disjunction (∨) and implication (→). Write ⊢ϕ to indicate that such a formula is intuitionistically valid. We show that for each variable p and formula ϕ there exists a formula Apϕ (effectively computable from ϕ), containing only variables not equal to p which occur in ϕ, and such that for all formulas ψ not involving p, ⊢ψ → Apϕ if and only if ⊢ψ → ϕ. Consequently quantification over propositional variables can be modelled in IpC, and there is an interpretation of the second order propositional calculus, IpC2, in IpC which restricts to the identity on first order propositions.An immediate corollary is the strengthening of the usual interpolation theorem for IpC to the statement that there are least and greatest interpolant formulas for any given pair of formulas. The result also has a number of interesting consequences for the algebraic counterpart of IpC, the theory of Heyting algebras. In particular we show that a model of IpC2 can be constructed whose algebra of truth-values is equal to any given Heyting algebra.

scholarly journals Atomic polymorphism

2013 ◽  
Vol 78 (1) ◽  
pp. 260-274 ◽  
Author(s):  
Fernando Ferreira ◽  
Gilda Ferreira
Keyword(s):  
Crucial Role ◽  
Propositional Calculus ◽  
Reduction Step ◽  
Strong Normalization ◽  
Intuitionistic Propositional Calculus ◽  
Polymorphic System ◽  
System F

AbstractIt has been known for six years that the restriction of Girard's polymorphic system F to atomic universal instantiations interprets the full fragment of the intuitionistic propositional calculus. We firstly observe that Tait's method of “convertibility” applies quite naturally to the proof of strong normalization of the restricted Girard system. We then show that each β-reduction step of the full intuitionistic propositional calculus translates into one or more βη-reduction steps in the restricted Girard system. As a consequence, we obtain a novel and perspicuous proof of the strong normalization property for the full intuitionistic propositional calculus. It is noticed that this novel proof bestows a crucial role to η-conversions.

Martin-Löf ’s type theory

2001 ◽  
Author(s):  
B. Nördstrom ◽  
K. Petersson
Keyword(s):  
Computer Program ◽  
Programming Language ◽  
Type Theory ◽  
Predicate Logic ◽  
Propositional Calculus ◽  
Constructive Proof ◽  
Intuitionistic Propositional Calculus ◽  
Problem Description ◽  
Program Construction ◽  
Correct Program

The type theory described in this chapter has been developed by Martin-Löf with the original aim of being a clarification of constructive mathematics. Unlike most other formalizations of mathematics, type theory is not based on predicate logic. Instead, the logical constants are interpreted within type theory through the Curry-Howard correspondence between propositions and sets [Curry and Feys, 1958; Howard, 1980]: a proposition is interpreted as a set whose elements represent the proofs of the proposition. It is also possible to view a set as a problem description in a way similar to Kolmogorov’s explanation of the intuitionistic propositional calculus [Kolmogorov, 1932]. In particular, a set can be seen as a specification of a programming problem; the elements of the set are then the programs that satisfy the specification. An advantage of using type theory for program construction is that it is possible to express both specifications and programs within the same formalism. Furthermore, the proof rules can be used to derive a correct program from a specification as well as to verify that a given program has a certain property. As a programming language, type theory is similar to typed functional languages such as ML [Gordon et al., 1979; Milner et al., 1990] and Haskell [Hudak et al, 1992], but a major difference is that the evaluation of a well-typed program always terminates. The notion of constructive proof is closely related to the notion of computer program. To prove a proposition ("x Î A)($yÎB)P(x,y) constructively means to give a function f which when applied to an element a in A gives an element b in B such that P(a, b) holds. So if the proposition ("xÎ A)($yÎB)P(x,y) expresses a specification, then the function f obtained from the proof is a program satisfying the specification. A constructive proof could therefore itself be seen as a computer program and the process of computing the value of a program corresponds to the process of normalizing a proof. It is by this computational content of a constructive proof that type theory can be used as a programming language; and since the program is obtained from a proof of its specification, type theory can be used as a programming logic.

Sign in / Sign up

Export Citation Format

Share Document