Normalization theorems for full first order classical natural deduction

1991 ◽  
Vol 56 (1) ◽  
pp. 129-149 ◽  
Author(s):  
Gunnar Stålmarck
Keyword(s):  
Normal Form ◽  
Natural Deduction ◽  
Full System ◽  
Strong Normalization ◽  
Logical Constants ◽  
Restricted Version ◽  
First Order ◽  
Form Theorem ◽  
Normalization Theorem ◽  
Normal Form Theorem

In this paper we prove the strong normalization theorem for full first order classical N.D. (natural deduction)—full in the sense that all logical constants are taken as primitive. We also give a syntactic proof of the normal form theorem and (weak) normalization for the same system.The theorem has been stated several times, and some proofs appear in the literature. The first proof occurs in Statman [1], where full first order classical N.D. (with the elimination rules for ∨ and ∃ restricted to atomic conclusions) is embedded in a system for second order (propositional) intuitionistic N.D., for which a strong normalization theorem is proved using strongly impredicative methods.A proof of the normal form theorem and (weak) normalization theorem occurs in Seldin [1] as an extension of a proof of the same theorem for an N.D.-system for the intermediate logic called MH.The proof of the strong normalization theorem presented in this paper is obtained by proving that a certain kind of validity applies to all derivations in the system considered.The notion “validity” is adopted from Prawitz [2], where it is used to prove the strong normalization theorem for a restricted version of first order classical N.D., and is extended to cover the full system. Notions similar to “validity” have been used earlier by Tait (convertability), Girard (réducibilité) and Martin-Löf (computability).In Prawitz [2] the N.D. system is restricted in the sense that ∨ and ∃ are not treated as primitive logical constants, and hence the deductions can only be seen to be “natural” with respect to the other logical constants. To spell it out, the strong normalization theorem for the restricted version of first order classical N.D. together with the well-known results on the definability of the rules for ∨ and ∃ in the restricted system does not imply the normalization theorem for the full system.

Proofs, Snakes and Ladders

Dialogue ◽  
1974 ◽  
Vol 13 (4) ◽  
pp. 723-731 ◽  
Author(s):  
Alasdair Urquhart
Keyword(s):  
Normal Form ◽  
Intuitionistic Logic ◽  
Natural Deduction ◽  
Tree Structure ◽  
Deduction System ◽  
Syntactical Structure ◽  
Form Theorem ◽  
Structural Identity ◽  
Natural Deduction System ◽  
Normal Form Theorem

Anyone who has worked at proving theorems of intuitionistic logic in a natural deduction system must have been struck by the way in which many logical theorems “prove themselves.” That is, proofs of many formulas can be read off from the syntactical structure of the formulas themselves. This observation suggests that perhaps a strong structural identity may underly this relation between formulas and their proofs. A formula can be considered as a tree structure composed of its subformulas (Frege 1879) and by the normal form theorem (Gentzen 1934) every formula has a normalized proof consisting of its subformulas. Might we not identify an intuitionistic theorem with (one of) its proof(s) in normal form?

scholarly journals Normal form theorem for systems of sequents

2007 ◽  
pp. 37-53
Author(s):  
Mirjana Borisavljevic
Keyword(s):  
Normal Form ◽  
Natural Deduction ◽  
Predicate Logic ◽  
Special Kind ◽  
Form Theorem ◽  
Normal Form Theorem

In a system of sequents for intuitionistic predicate logic a theorem, which corresponds to Prawitz?s Normal Form Theorem for natural deduction, are proved. In sequent derivations a special kind of cuts, maximum cuts, are defined. Maximum cuts from sequent derivations are connected with maximum segments from natural deduction derivations, i.e., sequent derivations without maximum cuts correspond to normal derivations in natural deduction. By that connection the theorem for the system of sequents (which correspond to Normal Form Theorem for natural deduction) will have the following form for each sequent derivation whose end sequent is ??A there is a sequent derivation without maximum cuts whose end sequent is ??A.

A normal form theorem for Lω1p, with applications

1982 ◽  
Vol 47 (3) ◽  
pp. 605-624 ◽  
Author(s):  
Douglas N. Hoover
Keyword(s):  
Normal Form ◽  
Probability Model ◽  
Random Variables ◽  
Interpolation Theorem ◽  
Complete Theory ◽  
De Finetti’S Theorem ◽  
Form Theorem ◽  
Normal Form Theorem ◽  
De Finetti's Theorem

AbstractWe show that every formula of Lω1P is equivalent to one which is a propositional combination of formulas with only one quantifier. It follows that the complete theory of a probability model is determined by the distribution of a family of random variables induced by the model. We characterize the class of distribution which can arise in such a way. We use these results together with a form of de Finetti’s theorem to prove an almost sure interpolation theorem for Lω1P.

scholarly journals Reduction in first-order logic compared with reduction in implicational logic

2007 ◽  
Vol 5 ◽  
Author(s):  
Tigran M. Galoyan
Keyword(s):  
Natural Deduction ◽  
Order Logic ◽  
First Order Logic ◽  
Strong Normalization ◽  
First Order ◽  
Reduction Sequence

In this paper we discuss strong normalization for natural deduction in the →∀-fragment of first-order logic. The method of collapsing types is used to transfer the result (concerning strong normalization) from implicational logic to first-order logic. The result is improved by a complement, which states that the length of any reduction sequence of derivation term r in first-order logic is equal to the length of the corresponding reduction sequence of its collapse term rc in implicational logic.

Refinements of Vaught's normal from theorem

1979 ◽  
Vol 44 (3) ◽  
pp. 289-306 ◽  
Author(s):  
Victor Harnik
Keyword(s):  
Normal Form ◽  
Boolean Combination ◽  
Form Theorem ◽  
Central Notion ◽  
The Matrix ◽  
Normal Form Theorem ◽  
Skolem Theorem ◽  
Image Position ◽  
Countable Models

The central notion of this paper is that of a (conjunctive) game-sentence, i.e., a sentence of the formwhere the indices ki, ji range over given countable sets and the matrix conjuncts are, say, open -formulas. Such game sentences were first considered, independently, by Svenonius [19], Moschovakis [13]—[15] and Vaught [20]. Other references are [1], [3]—[5], [10]—[12]. The following normal form theorem was proved by Vaught (and, in less general forms, by his predecessors).Theorem 0.1. Let L = L0(R). For every -sentence ϕ there is an L0-game sentence Θ such that ⊨′ ∃Rϕ ↔ Θ.(A word about the notations: L0(R) denotes the language obtained from L0 by adding to it the sequence R of logical symbols which do not belong to L0; “⊨′α” means that α is true in all countable models.)0.1 can be restated as follows.Theorem 0.1′. For every-sentence ϕ there is an L0-game sentence Θ such that ⊨ϕ → Θ and for any-sentence ϕ if ⊨ϕ → ϕ and L′ ⋂ L ⊆ L0, then ⊨ Θ → ϕ.(We sketch the proof of the equivalence between 0.1 and 0.1′.0.1 implies 0.1′. This is obvious once we realize that game sentences and their negations satisfy the downward Löwenheim-Skolem theorem and hence, ⊨′α is equivalent to ⊨α whenever α is a boolean combination of and game sentences.

An Abstract Birkhoff Normal Form Theorem and Exponential Type Stability of the 1d NLS

2019 ◽  
Vol 375 (3) ◽  
pp. 2089-2153 ◽  
Author(s):  
Luca Biasco ◽  
Jessica Elisa Massetti ◽  
Michela Procesi
Keyword(s):  
Normal Form ◽  
Exponential Type ◽  
Birkhoff Normal Form ◽  
Form Theorem ◽  
Normal Form Theorem

scholarly journals Implicational complexity in intuitionistic arithmetic

1981 ◽  
Vol 46 (2) ◽  
pp. 240-248 ◽  
Author(s):  
Daniel Leivant
Keyword(s):  
Normal Form ◽  
Form Theorem ◽  
Natural Measure ◽  
Normal Form Theorem ◽  
Propositional Constants ◽  
Image Position ◽  
Classical Arithmetic ◽  
Intuitionistic Arithmetic

In classical arithmetic a natural measure for the complexity of relations is provided by the number of quantifier alternations in an equivalent prenex normal form. However, the proof of the Prenex Normal Form Theorem uses the following intuitionistically invalid rules for permuting quantifiers with propositional constants.Each one of these schemas, when added to Intuitionistic (Heyting's) Arithmetic IA, generates full Classical (Peano's) Arithmetic. Schema (3) is of little interest here, since one can obtain a formula intuitionistically equivalent to A ∨ ∀xBx, which is prenex if A and B are:For the two conjuncts on the r.h.s. (1) may be successively applied, since y = 0 is decidable.We shall readily verify that there is no way of similarly going around (1) or (2). This fact calls for counting implication (though not conjunction or disjunction) in measuring in IA the complexity of arithmetic relations. The natural implicational measure for our purpose is the depth of negative nestings of implication, defined as follows. I(F): = 0 if F is atomic; I(F ∧ G) = I(F ∨ G): = max[I(F), I(G)]; I(∀xF) = I(∃xF): = I(F); I(F → G):= max[I(F) + 1, I(G)].

Sign in / Sign up

Export Citation Format

Share Document