Mediaspace scheduled maintenance: Aug 25, 2026 07:00 - 12:00 AM. During this time, videos will be temporarily unavailable. Check status updates.

Lecture

Proofs: Arguments in Predicate Logic

In course

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 as diverse as mathematical reasoning, combinatorics, disc ...

Description

This lecture covers the rules of inference for quantified statements, including universal instantiation, generalization, existential instantiation, generalization, and modus ponens. Through examples, the instructor demonstrates how to construct valid arguments using predicate logic.

Instructor

Karl Aberer

Karl Aberer received his PhD in mathematics in 1991 from the ETH Zürich. From 1991 to 1992 he was postdoctoral fellow at the International Computer Science Institute (ICSI) at the University of California, Berkeley. In 1992, he joined the Integrated Publication and Information Systems institute (IPSI) of GMD in Germany, where he was leading the research division Open Adaptive Information Management Systems. In 2000 he joined EPFL as full professor. Since 2005 he is the director of the Swiss National Research Center for Mobile Information and Communication Systems ( NCCR-MICS, www.mics.ch ). He is member of the editorial boards of VLDB Journal, ACM Transaction on Autonomous and Adaptive Systems and World Wide Web Journal. He has been consulting for the Swiss government in research and science policy as a member of the Swiss Research and Technology Council ( SWTR ) from 2003 - 2011.

Official source

Ontological neighbourhood

Logic

Classical logic: First-order logic

Related concepts (30)

Universal quantification

In mathematical logic, a universal quantification is a type of quantifier, a logical constant which is interpreted as "given any", "for all", or "for any". It expresses that a predicate can be satisfied by every member of a domain of discourse. In other words, it is the predication of a property or relation to every member of the domain. It asserts that a predicate within the scope of a universal quantifier is true of every value of a predicate variable.

Existential quantification

In predicate logic, an existential quantification is a type of quantifier, a logical constant which is interpreted as "there exists", "there is at least one", or "for some". It is usually denoted by the logical operator symbol ∃, which, when used together with a predicate variable, is called an existential quantifier ("∃x" or "∃(x)" or "(∃x)"). Existential quantification is distinct from universal quantification ("for all"), which asserts that the property or relation holds for all members of the domain.

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.

Universal instantiation

In predicate logic, universal instantiation (UI; also called universal specification or universal elimination, and sometimes confused with dictum de omni) is a valid rule of inference from a truth about each member of a class of individuals to the truth about a particular individual of that class. It is generally given as a quantification rule for the universal quantifier but it can also be encoded in an axiom schema. It is one of the basic principles used in quantification theory. Example: "All dogs are mammals.

Rule of inference

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.

Related lectures (34)

Proofs: Arguments in Predicate Logic

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

Untitled

Predicate Logic: Quantifiers, CNF, DNF

Covers Predicate Logic, focusing on Quantifiers, CNF, and DNF.

Predicate Logic: Translating Natural Language into Logic

Covers the translation of natural language sentences into predicate logic and the importance of quantifier order.

Predicate Logic: Universal and Existential Quantifier