Logical biconditional | EPFL Graph Search

In logic and mathematics, the logical biconditional, also known as material biconditional or equivalence or biimplication or bientaiment, is the logical connective used to conjoin two statements and to form the statement " if and only if " (often abbreviated as " iff "), where is known as the antecedent, and the consequent. Nowadays, notations to represent equivalence include . is logically equivalent to both and , and the XNOR (exclusive nor) boolean operator, which means "both or neither". Semantically, the only case where a logical biconditional is different from a material conditional is the case where the hypothesis (antecedent) is false but the conclusion (consequent) is true. In this case, the result is true for the conditional, but false for the biconditional. In the conceptual interpretation, P = Q means "All P's are Q's and all Q's are P's". In other words, the sets P and Q coincide: they are identical. However, this does not mean that P and Q need to have the same meaning (e.g., P could be "equiangular trilateral" and Q could be "equilateral triangle"). When phrased as a sentence, the antecedent is the subject and the consequent is the predicate of a universal affirmative proposition (e.g., in the phrase "all men are mortal", "men" is the subject and "mortal" is the predicate). In the propositional interpretation, means that P implies Q and Q implies P; in other words, the propositions are logically equivalent, in the sense that both are either jointly true or jointly false. Again, this does not mean that they need to have the same meaning, as P could be "the triangle ABC has two equal sides" and Q could be "the triangle ABC has two equal angles". In general, the antecedent is the premise, or the cause, and the consequent is the consequence. When an implication is translated by a hypothetical (or conditional) judgment, the antecedent is called the hypothesis (or the condition) and the consequent is called the thesis.

LISA – A Modern Proof System

Viktor Kuncak, Simon Guilloud, Sankalp Gambhir

We present LISA, a proof system and proof assistant for constructing proofs in schematic first-order logic and axiomatic set theory. The logical kernel of the system is a proof checker for first-order logic with equality and schematic predicate and fun ...

2023

On Polynomial Algorithms for Normalizing Formulas

Viktor Kuncak, Simon Guilloud, Mario Bucev

We propose a new approach for normalization and simplification of logical formulas. Our approach is based on algorithms for lattice-like structures. Specifically, we present two efficient algorithms for computing a normal form and deciding the word problem ...

2022

Six additional replies - one more chorus of the S3 ballad

Dominique Foray

This paper has been written as a response to 'Six additional questions about smart specialization: implications for regional innovation policy 4.0' by M. Benner. The paper starts with the argument that recent academic work has enabled considerable progress ...

ROUTLEDGE JOURNALS, TAYLOR & FRANCIS LTD2020