IFR

Question 1

What is the Difference between Classical Logic, Intuitionistic logic and Predicate Logic?

Answer 1

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.

Question 2

What is the De morgan law?

Answer 2

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

Question 3

How to prove something is true in lean?

Answer 3

constructor

Question 4

how to prove something if we have false as an assumption

Answer 4

cases h

Question 5

Explain the law of the excluded middle? and how do we access it in lean?

Answer 5

The law of the excluded middle states that for every proposition it is either true or false. it is accessed by using “open classical”

Question 6

Explain the law of contradiction?

Answer 6

It states that contradictory propositions cannot both be true in the same sense and at the same time

Question 7

What is the generic relation that can be applied to any type : equality?

Answer 7

reflexivity

Question 8

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?

Answer 8

rewrite h

Question 9

We can also have assumed an equality and want to use it in the other direction, how is that done in lean?

Answer 9

rewrite<-

Question 10

What does it mean for a relation to be reflexive?

Answer 10

Reflexive means that there is a relation R which all elements are related to themselves. Example -> (∀ x : A, x=x),

Question 11

What does it mean for a relation to be transitive?

Answer 11

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)

Question 12

What does it mean for a relation to be symmetric?

Answer 12

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)

Question 13

list is defined as an inductive type how is it?

Answer 13

inductive list (A : Type)
|nil = list
| cons : A -> list -> list

Question 14

bool is defined as an inductive type how is it?

Answer 14

inductive bool : Type
| ff : bool
|tt : bool

Question 15

natural numbers are defined as an inductive type, how is it?

Answer 15

inductive nat : Type
| zero : nat
| succ : nat → nat

Question 16

what is commutative in maths?

Answer 16

Changing the order of the operands does not change the result. (addition and multiplication) ex 3+2 = 2+3

Question 17

what is associativity in maths?

Answer 17

Changing the grouping of addends does not change the sum. ( 2 + 3 ) + 4 = 2 + ( 3 + 4 )

Question 18

What is anti-symmetry in maths?

Answer 18

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)

Question 19

What is a monoid?

Answer 19

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.

Question 20

what is a partial order?

Answer 20

a partial order is a relation which is reflexive, transitive and antisymmetric.

Question 21

What De Morgan law is not provable in Intuitionistic logic?

Answer 21

¬ (P ∧ Q) ↔ ¬ P ∨ ¬ Q | only provable in classical logic.

Question 22

What is a neutral element?

Answer 22

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

Question 23

Define exponentiation in lean

Answer 23

def exp : ℕ → ℕ → ℕ
| n (succ m) := exp n m * n

n zero := 1

Question 24

What is an inverse element?

Answer 24

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

Question 25

What is distributivity

Answer 25

It involves how one operation (like addition or multiplication) interacts with another operation over a set of numbers.

a(b+c) = ba + c*a

Question 26

What is an injective function?

Answer 26

Every element of the function’s codomain is the image of at most one element of its domain.

Question 27

What are the properties of Natural numbers?

Answer 27

0 != succ(n) and succ is injective

Question 28

What are the properties of Lists?

Answer 28

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

Question 29

What is funext?

Answer 29

Is used to prove two functions are equal by showing that they produce the same outputs for all inputs

Question 30

What is a category?

Answer 30

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