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
What is distributivity
It involves how one operation (like addition or multiplication) interacts with another operation over a set of numbers.
a(b+c) = ba + c*a
What is an injective function?
Every element of the function’s codomain is the image of at most one element of its domain.
What are the properties of Natural numbers?
0 != succ(n) and succ is injective
What are the properties of Lists?
Similarly to Natural Numbers -> nil != a (no-confusion rules)
cons is injective, i.e. given cons a as = cons b bs then we know that a = b and as = bs.
append(++) is a monoid
What is funext?
Is used to prove two functions are equal by showing that they produce the same outputs for all inputs
What is a category?
Is if an equation doesn’t have an exact type on which the operations are defined but a whole family of types. This structure is called category
