Universal generalization

In predicate logic, generalization (also universal generalization or universal introduction, GEN) is a valid inference rule. It states that if has been derived, then can be derived. The full generalization rule allows for hypotheses to the left of the turnstile, but with restrictions. Assume is a set of formulas, a formula, and has been derived. The generalization rule states that can be derived if is not mentioned in and does not occur in . These restrictions are necessary for soundness. Without the first restriction, one could conclude from the hypothesis . Without the second restriction, one could make the following deduction: (Hypothesis) (Existential instantiation) (Existential instantiation) (Faulty universal generalization) This purports to show that which is an unsound deduction. Note that is permissible if is not mentioned in (the second restriction need not apply, as the semantic structure of is not being changed by the substitution of any variables). Prove: is derivable from and . Proof: In this proof, universal generalization was used in step 8. The deduction theorem was applicable in steps 10 and 11 because the formulas being moved have no free variables.

About this result

This page is automatically generated and may contain information that is not correct, complete, up-to-date, or relevant to your search query. The same applies to every other page on this website. Please make sure to verify the information with EPFL's official sources.

Related publications (1)

Related concepts (2)

Related courses (1)

Related lectures (6)

CS-101: Advanced information, computation, communication I

Discrete mathematics is a discipline with applications to almost all areas of study. It provides a set of indispensable tools to computer science in particular. This course reviews (familiar) topics a

A note on universal inference

Anthony Christopher Davison, Timmy Rong Tian Tse

Universal inference enables the construction of confidence intervals and tests without regularity conditions by splitting the data into two parts and appealing to Markov's inequality. Previous investigations have shown that the cost of this generality is a ...

WILEY2022

In mathematical physics, Hilbert system is an infrequently used term for a physical system described by a C*-algebra. In logic, especially mathematical logic, a Hilbert system, sometimes called Hilbert calculus, Hilbert-style deductive system or Hilbert–Ackermann system, is a type of system of formal deduction attributed to Gottlob Frege and David Hilbert. These deductive systems are most often studied for first-order logic, but are of interest for other logics as well.

In philosophy of logic and logic, a rule of inference, inference rule or transformation rule is a logical form consisting of a function which takes premises, analyzes their syntax, and returns a conclusion (or conclusions). For example, the rule of inference called modus ponens takes two premises, one in the form "If p then q" and another in the form "p", and returns the conclusion "q". The rule is valid with respect to the semantics of classical logic (as well as the semantics of many other non-classical logics), in the sense that if the premises are true (under an interpretation), then so is the conclusion.

Proofs: Arguments in Predicate Logic CS-101: Advanced information, computation, communication I

Covers rules of inference for quantified statements and constructing valid arguments using predicate logic.

Proofs: Arguments in Predicate Logic CS-101: Advanced information, computation, communication I

Covers rules of inference for quantified statements and demonstrates constructing valid arguments using predicate logic.

Automating First-Order Logic Proofs Using Resolution CS-550: Formal verification

Covers first-order logic syntax, semantics, Skolemization, resolution, and normal form transformations.