IFR Flashcards
What is the Difference between Classical Logic, Intuitionistic logic and Predicate Logic?
Classical Logic is the most traditional form of logic with the law of em and proof by contradiction. Intuitionistic logic is a more constructive logic that rejects the law of em. Predicate logic extends classical or intuitionistic logic to handle more complex statement involving variables and quantifiers.
What is the De morgan law?
The De morgan law states that if you negate a conjunction or a disjunction it is equivalent to negation of their components with disjunction replaced by conjunction and vice-versa.
¬ (P ∨ Q) ↔ ¬ P ∧ ¬ Q
¬ (P ∧ Q) ↔ ¬ P ∨ ¬ Q
How to prove something is true in lean?
constructor
how to prove something if we have false as an assumption
cases h
Explain the law of the excluded middle? and how do we access it in lean?
The law of the excluded middle states that for every proposition it is either true or false. it is accessed by using “open classical”
Explain the law of contradiction?
It states that contradictory propositions cannot both be true in the same sense and at the same time
What is the generic relation that can be applied to any type : equality?
reflexivity
However, if we have assumed an equality what can we use if we have h : a = b, that is if our Goal is PP a we say ….. h to change it to PP b?
rewrite h
We can also have assumed an equality and want to use it in the other direction, how is that done in lean?
rewrite<-
What does it mean for a relation to be reflexive?
Reflexive means that there is a relation R which all elements are related to themselves. Example -> (∀ x : A, x=x),
What does it mean for a relation to be transitive?
Transitive means that whenever there is a relation R which have pairs (a,b) it implies the relation (b,c) which says that If A is related to B, and B is related to C, then A is related to C. | Example -> (∀ x y z : A, x=y → y=z → x=z)
What does it mean for a relation to be symmetric?
Symmetric means that whenever elements are related in pairs (a,b) it implies the relation between (b,a) |Example -> (∀ x y : A, x=y → y=x)
list is defined as an inductive type how is it?
inductive list (A : Type)
|nil = list
| cons : A -> list -> list
bool is defined as an inductive type how is it?
inductive bool : Type
| ff : bool
|tt : bool
natural numbers are defined as an inductive type, how is it?
inductive nat : Type
| zero : nat
| succ : nat → nat
what is commutative in maths?
Changing the order of the operands does not change the result. (addition and multiplication) ex 3+2 = 2+3
what is associativity in maths?
Changing the grouping of addends does not change the sum. ( 2 + 3 ) + 4 = 2 + ( 3 + 4 )
What is anti-symmetry in maths?
if there is a relation from a to b, and there is also a relation from b to a, then a must be equal to b for the relation to be antisymmetric
antisymmetry (∀ x y : ℕ , x ≤ y → y ≤ x → x = y)
What is a monoid?
Let M be a set, and let :M×M→M be a binary operation.
Associativity: For all elements a,b,c in M the operation is associative, meaning (ab)c = a(bc)
Identity Element Or Neutral Element: There exists an element e in M such that for any element a in M, the operation with the identity element is the element itself, i.e., = e∗a=a∗e=a.
what is a partial order?
a partial order is a relation which is reflexive, transitive and antisymmetric.
What De Morgan law is not provable in Intuitionistic logic?
¬ (P ∧ Q) ↔ ¬ P ∨ ¬ Q | only provable in classical logic.
What is a neutral element?
an element that leaves unchanged every element when the operation is applied. In multiplication is 1 and in addition is 0, e.g. x*1 = x and 1 * x = x same with addition 0+x = x and x + 0 = x
Define exponentiation in lean
def exp : ℕ → ℕ → ℕ
| n (succ m) := exp n m * n
n zero := 1
What is an inverse element?
An inverse element in a mathematical structure is a special element that, when combined with another element using a given operation, results in the identity element for that operation . ->
𝑥+(−𝑥)=0 and −𝑥+𝑥=0
