On the definition of ‘formal deduction’

1956 ◽  
Vol 21 (2) ◽  
pp. 129-136 ◽  
Author(s):  
Richard Montague ◽  
Leon Henkin
Keyword(s):  
Functional Calculus ◽  
Modus Ponens ◽  
Formal Proof ◽  
Axiom Schema ◽  
First Order ◽  
Individual Variable ◽  
Individual Variables ◽  
Definition Of ◽  
Formal Rules

The following remarks apply to many functional calculi, each of which can be variously axiomatized, but for clarity of exposition we shall confine our attention to one particular system Σ. This system is to have the usual primitive symbols and formation rules of the pure first-order functional calculus, and the following formal axiom schemata and formal rules of inference.Axiom schema 1. Any tautologous wff (well-formed formula).Axiom schema 2. (a) A ⊃ B, where A is any wff, a and b are any individual variables, and B arises from A by replacing all free occurrences of a by free occurrences of b.Axiom schema 3. (a)(A ⊃ B)⊃(A⊃ (a)B). where A and B are any wffs, and a is any individual variable not free in A.Rule of Modus Ponens: applies to wffs A and A ⊃ B, and yields B.Rule of Generalization: applies to a wff A and yields (a)A, where a is any individual variable.A formal proof in Σ is a finite column of wffs each of whose lines is a formal axiom or arises from two preceding lines by the Rule of Modus Ponens or arises from a single preceding line by the Rule of Generalization. A formal theorem of Σ is a wff which occurs as the last line of some formal proof.

On the rules of proof in the pure functional calculus of the first order

1951 ◽  
Vol 16 (2) ◽  
pp. 107-111 ◽  
Author(s):  
Andrzej Mostowski
Keyword(s):  
Functional Calculus ◽  
Free Variable ◽  
Propositional Function ◽  
Cartesian Power ◽  
First Order ◽  
A Value ◽  
Free Variables ◽  
Individual Variables ◽  
Definition Of

We consider here the pure functional calculus of first order as formulated by Church.Church, l.c., p. 79, gives the definition of the validity of a formula in a given set I of individuals and shows that a formula is provable in if and only if it is valid in every non-empty set I. The definition of validity is preceded by the definition of a value of a formula; the notion of a value is the basic “semantical” notion in terms of which all other semantical notions are definable.The notion of a value of a formula retains its meaning also in the case when the set I is empty. We have only to remember that if I is empty, then an m-ary propositional function (i.e. a function from the m-th cartesian power Im to the set {f, t}) is the empty set. It then follows easily that the value of each well-formed formula with free individual variables is the empty set. The values of wffs without free variables are on the contrary either f or t. Indeed, if B has the unique free variable c and ϕ is the value of B, then the value of (c)B according to the definition given by Church is the propositional constant f or t according as ϕ(j) is f for at least one j in I or not. Since, however, there is no j in I, the condition ϕ(j) = t for all j in I is vacuously satisfied and hence the value of (c)B is t.

Completeness in the theory of types

1950 ◽  
Vol 15 (2) ◽  
pp. 81-91 ◽  
Author(s):  
Leon Henkin
Keyword(s):  
Functional Calculus ◽  
Formal System ◽  
Axiom System ◽  
Second Order ◽  
True Proposition ◽  
Arbitrary Domain ◽  
Individual Variables ◽  
Definition Of ◽  
The Individual ◽  
Positive Integers

The first order functional calculus was proved complete by Gödel in 1930. Roughly speaking, this proof demonstrates that each formula of the calculus is a formal theorem which becomes a true sentence under every one of a certain intended class of interpretations of the formal system.For the functional calculus of second order, in which predicate variables may be bound, a very different kind of result is known: no matter what (recursive) set of axioms are chosen, the system will contain a formula which is valid but not a formal theorem. This follows from results of Gödel concerning systems containing a theory of natural numbers, because a finite categorical set of axioms for the positive integers can be formulated within a second order calculus to which a functional constant has been added.By a valid formula of the second order calculus is meant one which expresses a true proposition whenever the individual variables are interpreted as ranging over an (arbitrary) domain of elements while the functional variables of degree n range over all sets of ordered n-tuples of individuals. Under this definition of validity, we must conclude from Gödel's results that the calculus is essentially incomplete.It happens, however, that there is a wider class of models which furnish an interpretation for the symbolism of the calculus consistent with the usual axioms and formal rules of inference. Roughly, these models consist of an arbitrary domain of individuals, as before, but now an arbitrary class of sets of ordered n-tuples of individuals as the range for functional variables of degree n. If we redefine the notion of valid formula to mean one which expresses a true proposition with respect to every one of these models, we can then prove that the usual axiom system for the second order calculus is complete: a formula is valid if and only if it is a formal theorem.

scholarly journals Formalization Of Theories of Design Using: First Order Logic Augmented With A Causal Calculus; And Entropy of a Design Defined In Terms Of The Function, Behavior and Structure Ontology.

2021 ◽  
Author(s):  
KARTHIK GURUMURTHI
Keyword(s):  
High Probability ◽  
Formal Proof ◽  
Order Logic ◽  
First Order Logic ◽  
Logical Framework ◽  
Seamless Integration ◽  
Good Design ◽  
First Order ◽  
Individual Variables ◽  
And Behavior

A symbolic logical framework (L) consisting of first order logic augmented with a causal calculus has been provided to formalize, axiomatize and integrate theories of design. L is used to represent designs in the Function-Behavior-Structure (FBS) ontology in a single, widely applicable language that enables the following: seamless integration of representations of function, behavior and structure; and generality in the formalization of theories of design. FRs, constraints, structure and behavior are represented as sentences in L. FRs are represented (as abstractions of behavior) in the form of existentially quantified sentences, the instantiation of whose individual variables yields the representation of behavior. This enables the logical implication of FRs by behavior, without recourse to apriori criteria for satisfaction of FRs by behavior. Functional decomposition is represented to enable lower level FRs to logically imply the satisfaction of higher level FRs. The theory of whether and how structure and behavior satisfy FRs and constraints is represented as a formal proof in L. Important general attributes of designs such as solution-neutrality of FRs, probability of satisfaction of requirements and constraints (calculated in a Bayesian framework using Monte Carlo simulation), extent and nature of coupling, etc. have been defined in terms of the representation of a design in L. The entropy of a design is defined in terms of the above attributes of a design, based on which a general theory of what constitutes a good design has been formalized to include the desirability of solution-neutrality of (especially higher level) FRs, high probability of satisfaction of requirements and constraints, wide specifications, low variability and bias, use of fewer attributes to specify the design, less coupling (especially circular coupling at higher levels of FRs), parametrization, standardization, etc..

A relative consistency proof

1954 ◽  
Vol 19 (1) ◽  
pp. 21-28 ◽  
Author(s):  
Joseph R. Shoenfield
Keyword(s):  
Set Theory ◽  
Functional Calculus ◽  
Direct Method ◽  
Axiom System ◽  
Similar Process ◽  
Consistency Proof ◽  
First Order ◽  
Definition Of ◽  
A Direct Method ◽  
Exact Definition

LetCbe an axiom system formalized within the first order functional calculus, and letC′ be related toCas the Bernays-Gödel set theory is related to the Zermelo-Fraenkel set theory. (An exact definition ofC′ will be given later.) Ilse Novak [5] and Mostowski [8] have shown that, ifCis consistent, thenC′ is consistent. (The converse is obvious.) Mostowski has also proved the stronger result that any theorem ofC′ which can be formalized inCis a theorem ofC.The proofs of Novak and Mostowski do not provide a direct method for obtaining a contradiction inCfrom a contradiction inC′. We could, of course, obtain such a contradiction by proving the theorems ofCone by one; the above result assures us that we must eventually obtain a contradiction. A similar process is necessary to obtain the proof of a theorem inCfrom its proof inC′. The purpose of this paper is to give a new proof of these theorems which provides a direct method of obtaining the desired contradiction or proof.The advantage of the proof may be stated more specifically by arithmetizing the syntax ofCandC′.

A generalization of the concept of ω-consistency

1954 ◽  
Vol 19 (3) ◽  
pp. 183-196 ◽  
Author(s):  
Leon Henkin
Keyword(s):  
Functional Calculus ◽  
Free Variable ◽  
Natural Numbers ◽  
Deductive Systems ◽  
Individual Variable ◽  
Special Cases ◽  
Definition Of ◽  
The Individual ◽  
Formal Properties ◽  
Use Of Models

In this paper we consider certain formal properties of deductive systems which, in special cases, reduce to the property of ω-consistency; and we then seek to understand the significance of these properties by relating them to the use of models in providing interpretations of the deductive systems.The notion of ω-consistency arises in connection with deductive systems of arithmetic. For definiteness, let us suppose that the system is a functional calculus whose domain of individuals is construed as the set of natural numbers, and that the system possesses individual constants ν0, ν1, ν2, … such that νi functions as a name for the number i. Such a system is called ω-consistent, if there is no well-formed formula A(x) (in which x is the only free variable) such that A(ν0), A(ν1), A(ν2), … and ∼(x)A(x) are all formal theorems of the system, where A(νi) is the formula resulting from A(x) by substituting the constant νi for each free occurrence of the individual variable x.Now consider an arbitrary applied functional calculus F, and let Γ be any non-empty set of its individual constants. In imitation of the definition of ω-consistency, we may say that the system F is Γ-consistent, if it contains no formula A(x) (in which x is the only free variable) such that ⊦ A (α) for every constant α in Γ, and also ⊦ ∼(x)A(x) (where an occurrence of “⊦” indicates that the formula which it precedes is a formal theorem). We easily see that the condition of Γ-consistency is equivalent to the condition that the system F contain no formula B(x) such that ⊦ ∼ B(α) for each α in Γ, and also ⊦ (∃x)B(x).

A note on direct products

1958 ◽  
Vol 23 (1) ◽  
pp. 1-6 ◽  
Author(s):  
L. Novak Gál
Keyword(s):  
Binary Relation ◽  
Direct Product ◽  
Functional Calculus ◽  
Ordered Set ◽  
Infinite Sequence ◽  
Direct Products ◽  
First Order ◽  
Individual Variables ◽  
The Individual ◽  
Infinite Sequences

By an algebra is meant an ordered set Γ = 〈V,R1, …, Rn, O1, …, Om〉, where V is a class, Ri (1 ≤ i ≤, n) is a relation on nj elements of V (i.e. Ri ⊆ Vni), and Oj (1 ≤ i ≤ n) is an operation on elements of V such that Oj(x1, … xmj) ∈ V) for all x1, …, xmj ∈ V). A sentence S of the first-order functional calculus is valid in Γ, if it contains just individual variables x1, x2, …, relation variables ϱ1, …,ϱn, where ϱi,- is nj-ary (1 ≤ i ≤ n), and operation variables σ1, …, σm, where σj is mj-ary (1 ≤, j ≤ m), and S holds if the individual variables are interpreted as ranging over V, ϱi is interpreted as Ri, and σi as Oj. If {Γi}i≤α is a (finite or infinite) sequence of algebras Γi, where Γi = 〈Vi, Ri〉 and Ri, is a binary relation, then by the direct productΓ = Πi<αΓi is meant the algebra Γ = 〈V, R〉, where V consists of all (finite or infinite) sequences x = 〈x1, x2, …, xi, …〉 with Xi ∈ Vi and where R is a binary relation such that two elements x and y of V are in the relation R if and only if xi and yi- are in the relation Ri for each i < α.

scholarly journals A FORMALIZATION OF KANT’S TRANSCENDENTAL LOGIC

2011 ◽  
Vol 4 (2) ◽  
pp. 254-289 ◽  
Author(s):  
T. ACHOURIOTI ◽  
M. VAN LAMBALGEN
Keyword(s):  
Formal Proof ◽  
Order Logic ◽  
First Order Logic ◽  
Pure Reason ◽  
Critique Of Pure Reason ◽  
Technical Application ◽  
First Order ◽  
Transcendental Logic ◽  
Definition Of ◽  
Argumentative Structure

Although Kant (1998) envisaged a prominent role for logic in the argumentative structure of his Critique of Pure Reason, logicians and philosophers have generally judged Kant’s logic negatively. What Kant called ‘general’ or ‘formal’ logic has been dismissed as a fairly arbitrary subsystem of first-order logic, and what he called ‘transcendental logic’ is considered to be not a logic at all: no syntax, no semantics, no definition of validity. Against this, we argue that Kant’s ‘transcendental logic’ is a logic in the strict formal sense, albeit with a semantics and a definition of validity that are vastly more complex than that of first-order logic. The main technical application of the formalism developed here is a formal proof that Kant’s Table of Judgements in Section 9 of the Critique of Pure Reason, is indeed, as Kant claimed, complete for the kind of semantics he had in mind. This result implies that Kant’s ‘general’ logic is after all a distinguished subsystem of first-order logic, namely what is known as geometric logic.

All or none; A novel choice of primitives for elementary logic

1967 ◽  
Vol 32 (3) ◽  
pp. 345-351 ◽  
Author(s):  
R. H. Thomason ◽  
H. Leblanc
Keyword(s):  
Propositional Variable ◽  
First Order ◽  
Individual Variable ◽  
Definition Of ◽  
Predicate Variable

In [1] Ludwik Borkowski takes a quantifier symbol ‘Q1’ (e.g., the familiar ‘∀’) to permit definition of another quantifier symbol ‘Q1’ if, where ‘f’ is a singulary predicate variable, there exists a formula A of QC1—a first-order quantificational calculus (without identity and individual constants) having ‘Q1’ as its one primitive quantifier symbol—such that: (1) under the intended interpretations of ‘Q1’ and ‘Q1’ the biconditional (Q1X)f(X) = A is valid, (2) no individual variable occurs free in A, and (3) A contains no propositional variable, and no predicate variable other than ‘f.’

A model theoretic approach to Malcev conditions

1977 ◽  
Vol 42 (2) ◽  
pp. 277-288 ◽  
Author(s):  
John T. Baldwin ◽  
Joel Berman
Keyword(s):  
Extensive Study ◽  
Second Order ◽  
Theoretic Approach ◽  
Easy Consequence ◽  
First Order ◽  
Congruence Relations ◽  
Individual Variables ◽  
Definition Of ◽  
The Individual ◽  
Necessary And Sufficient

A varietyV(equational class of algebras) satisfies a strong Malcev condition ∃f1,…, ∃fnθ(f1, …,fn,x1, …,xm) where θ is a conjunction of equations in the function variablesf1, …,fnand the individual variablesx1, …,xm, if there are polynomial symbolsp1, …,pnin the language ofVsuch that ∀x1, …,xmθ(p1…,pn,x1, …,xm) is a law ofV. Thus a strong Malcev condition involves restricted second order quantification of a strange sort. The quantification is restricted to functions which are “polynomially definable”. This notion was introduced by Malcev [6] who used it to describe those varieties all of whose members have permutable congruence relations. The general formal definition of Malcev conditions is due to Grätzer [1]. Since then and especially since Jónsson's [3] characterization of varieties with distributive congruences there has been extensive study of strong Malcev conditions and the related concepts: Malcev conditions and weak Malcev conditions.In [9], Taylor gives necessary and sufficient semantic conditions for a class of varieties to be defined by a (strong) Malcev condition. A key to the proof is the translation of the restricted second order concepts into first order concepts in a certain many sorted language. In this paper we show that, given this translation, Taylor's theorem is an easy consequence of a result of Tarski [8] and the standard preservation theorems of first order logic.

UNIFICATION IN SUPERINTUITIONISTIC PREDICATE LOGICS AND ITS APPLICATIONS

2018 ◽  
Vol 12 (1) ◽  
pp. 37-61 ◽  
Author(s):  
WOJCIECH DZIK ◽  
PIOTR WOJTYLAK
Keyword(s):  
Propositional Logic ◽  
Predicate Logic ◽  
Order Logic ◽  
Existential Quantifier ◽  
First Order ◽  
Admissible Rules ◽  
Structural Completeness ◽  
Individual Variables ◽  
Definition Of ◽  
Finitely Presented

AbstractWe introduce unification in first-order logic. In propositional logic, unification was introduced by S. Ghilardi, see Ghilardi (1997, 1999, 2000). He successfully applied it in solving systematically the problem of admissibility of inference rules in intuitionistic and transitive modal propositional logics. Here we focus on superintuitionistic predicate logics and apply unification to some old and new problems: definability of disjunction and existential quantifier, disjunction and existential quantifier under implication, admissible rules, a basis for the passive rules, (almost) structural completeness, etc. For this aim we apply modified specific notions, introduced in propositional logic by Ghilardi, such as projective formulas, projective unifiers, etc.Unification in predicate logic seems to be harder than in the propositional case. Any definition of the key concept of substitution for predicate variables must take care of individual variables. We allow adding new free individual variables by substitutions (contrary to Pogorzelski & Prucnal (1975)). Moreover, since predicate logic is not as close to algebra as propositional logic, direct application of useful algebraic notions of finitely presented algebras, projective algebras, etc., is not possible.

Sign in / Sign up

Export Citation Format

Share Document