Herbrand's Theorem, Skolemization and Proof Systems for First-Order Lukasiewicz Logic

2008 ◽  
Vol 20 (1) ◽  
pp. 35-54 ◽  
Author(s):  
M. Baaz ◽  
G. Metcalfe
Keyword(s):  
Łukasiewicz Logic ◽  
First Order ◽  
Proof Systems ◽  
Lukasiewicz Logic ◽  
Herbrand’S Theorem ◽  
Herbrand's Theorem

Łukasiewicz Logic: From Proof Systems To Logic Programming

2005 ◽  
Vol 13 (5) ◽  
pp. 561-585 ◽  
Author(s):  
George Metcalfe ◽  
Nicola Olivetti ◽  
Dov Gabbay
Keyword(s):  
Logic Programming ◽  
Łukasiewicz Logic ◽  
Proof Systems ◽  
Lukasiewicz Logic

Compactness in first order Lukasiewicz logic

2011 ◽  
Vol 20 (1) ◽  
pp. 254-265 ◽  
Author(s):  
N. R. Tavana ◽  
M. Pourmahdian ◽  
F. Didehvar
Keyword(s):  
Łukasiewicz Logic ◽  
First Order ◽  
Lukasiewicz Logic

scholarly journals HERBRAND’S THEOREM AND NON-EUCLIDEAN GEOMETRY

2015 ◽  
Vol 21 (2) ◽  
pp. 111-122 ◽  
Author(s):  
MICHAEL BEESON ◽  
PIERRE BOUTRY ◽  
JULIEN NARBOUX
Keyword(s):  
Euclidean Geometry ◽  
The Other ◽  
Basic Theorem ◽  
Very Old ◽  
First Order ◽  
Herbrand’S Theorem ◽  
Non Euclidean Geometry ◽  
Herbrand's Theorem

AbstractWe use Herbrand’s theorem to give a new proof that Euclid’s parallel axiom is not derivable from the other axioms of first-order Euclidean geometry. Previous proofs involve constructing models of non-Euclidean geometry. This proof uses a very old and basic theorem of logic together with some simple properties of ruler-and-compass constructions to give a short, simple, and intuitively appealing proof.

A strong version of Herbrand's theorem for introvert sentences

1998 ◽  
Vol 63 (2) ◽  
pp. 555-569 ◽  
Author(s):  
Tore Langholm
Keyword(s):  
Ground Term ◽  
New Members ◽  
First Order ◽  
Herbrand’S Theorem ◽  
Universal Sentence ◽  
Order Language ◽  
The Matrix ◽  
Image Position ◽  
Infinite Set ◽  
Herbrand's Theorem

A version of Herbrand's theorem tells us that a universal sentence of a first-order language with at least one constant is satisfiable if and only if the conjunction of all its ground instances is. In general the set of such instances is infinite, and arbitrarily large finite subsets may have to be inspected in order to detect inconsistency. Essentially, the reason that every member of such an infinite set may potentially matter, can be traced back to sentences like(1) Loosely put, such sentences effectively sabotage any attempt to build a model from below in a finite number of steps, since new members of the Herbrand universe are constantly brought to attention. Since they cause an indefinite expansion of the relevant part of the Herbrand universe, such sentences could quite appropriately be called expanding.When such sentences are banned, stronger versions of Herbrand's theorem can be stated. Define a clause (disjunction of literals) to be non-expanding if every non-ground term occurring in a positive literal also occurs (possibly as an embedded subterm) in a negative literal of the same clause. Written as a disjunction of literals, the matrix of (1) clearly fails this criterion. Moreover, say that a sentence is non-expanding if it is a universal sentence with a quantifier-free matrix that is a conjunction of non-expanding clauses. Such sentences do in a sense never reach out beyond themselves, and the relevant part of the Herbrand universe is therefore drastically reduced.

Linear reasoning. A new form of the Herbrand-Gentzen theorem

1957 ◽  
Vol 22 (3) ◽  
pp. 250-268 ◽  
Author(s):  
William Craig
Keyword(s):  
Normal Form ◽  
Distinctive Feature ◽  
First Order ◽  
Herbrand’S Theorem ◽  
Free Level ◽  
New Form ◽  
The Relationship ◽  
Herbrand's Theorem

In Herbrand's Theorem [2] or Gentzen's Extended Hauptsatz [1], a certain relationship is asserted to hold between the structures of A and A′, whenever A implies A′ (i.e., A ⊃ A′ is valid) and moreover A is a conjunction and A′ an alternation of first-order formulas in prenex normal form. Unfortunately, the relationship is described in a roundabout way, by relating A and A′ to a quantifier-free tautology. One purpose of this paper is to provide a description which in certain respects is more direct. Roughly speaking, ascent to A ⊃ A′ from a quantifier-free level will be replaced by movement from A to A′ on the quantificational level. Each movement will be closely related to the ascent it replaces.The new description makes use of a set L of rules of inference, the L-rules. L is complete in the sense that, if A is a conjunction and A′ an alternation of first-order formulas in prenex normal form, and if A ⊃ A′ is valid, then A′ can be obtained from A by an L-deduction, i.e., by applications of L-rules only. The distinctive feature of L is that each L-rule possesses two characteristics which, especially in combination, are desirable. First, each L-rule yields only conclusions implied by the premisses.

Sign in / Sign up

Export Citation Format

Share Document