« first day (1062 days earlier)      last day (1419 days later) » 

F. Zer
F. Zer
17:59
(Q10):
	∀ x,y,z ∈ G ( x*(y*z) = (x*y)*z ) ∧ ∀ x,y ∈ G ( x *i(x) = y*i(y) ) ∧ ∀ x ∈ G ( x*(x*i(x)) = x ) ⇒ ∀ x,y ∈ G ( (i(y)*y)*x = x), where (infix) * : G^2 -> G and i : G -> G.
	If ∀ x,y,z ∈ G ( x*(y*z) = (x*y)*z ) ∧ ∀ x,y ∈ G ( x *i(x) = y*i(y) ) ∧ ∀ x ∈ G ( x*(x*i(x)) = x ):
		Given a ∈ G:
			Given b ∈ G:
				∀ x,y,z ∈ G ( x*(y*z) = (x*y)*z )
				∀ x,y ∈ G ( x *i(x) = y*i(y) )
				∀ x ∈ G ( x*(x*i(x)) = x )
				a*(a*i(a)) = a
				a*i(a) = b*i(b)
				a*(b*i(b)) = a
				...
Hi, @user21820. In case you celebrate it; Happy Easter !
@user21820 I have a similar problem with Q10; is there a commutative property missing ?
user21820
user21820
@F.Zer Well so my (Q9) had a bug, and indeed it can be fixed by having an extra condition such as ∀x,y∈L ( m(x,y) = m(y,x) ). However, I think it's way too easy, so I'm going to take that exercise out and replace by another one.
@F.Zer But no, (Q10) has no missing commutativity; that is what is hard about it. I checked it twice already (once last time and once just now) and it is correct. The proof is much shorter than that of (Q8) but is quite hard to find.
user21820
user21820
18:29
@F.Zer: Let me know when you decide that you want a hint for (Q10). I will tell you when I have decided on a replacement for (Q9).
F. Zer
F. Zer
@user21820, thank you for confirming ! It will work on Q10.
user21820
user21820
19:23
@F.Zer: Ok I've found a nice replacement. Here is the updated list of all the exercises:
PL (Propositional Logic):
(P1) A∨B∧C ⇔ (A∨B)∧(A∨C).
(P2) (A∨B)∧(B∨C)∧(C∨A) ⇒ (A∧B )∨(B∧C)∨(C∧A).
(P3) ( A ⇒ ¬B ) ∧ B ⇒ ¬A.
(P4) ¬(A∨B) ⇔ ¬A∧¬B.
(P5) ¬(A∧B) ⇔ ¬A∨¬B.
(P6) ( A ⇒ B ) ∨ ( B ⇒ A ).
(P7) ( A ⇒ B∨C ) ⇒ ( A ⇒ B ) ∨ ( A ⇒ C ).
FOL (First-Order Logic):
For (Q1) to (Q5), S is a type, and P is a property, and Q is a 2-parameter property (i.e. "Q(x,y)" is a statement about "x" and "y").
(Q1) ¬∀x∈S ( P(x) ) ⇒ ∃x∈S ( ¬P(x) ).
(Q2) ¬∃x∈S ( P(x) ) ⇒ ∀x∈S ( ¬P(x) ).
(Q3) ∃x∈S ( x∈S ) ⇒ ∃x∈S ( P(x) ⇒ ∀y∈S ( P(y) ) ).
(Q4) ∀x,y,z∈S ( x=z ∧ y=z ⇒ x=y ).
(Q5) ∀x∈S ( ∀y∈S ( Q(x,y) ⇒ P(x) ) ) iff ∀x∈S ( ∃y∈S ( Q(x,y) ) ⇒ P(x) ).
For (Q6) to (Q10), S,T,B,V,G are types, and "f : S→T" denotes "f is a 1-input function-symbol whose input must be of type S and whose output is of type T, and "f : S^2→T" denotes "f is a 2-input function-symbol whose inputs are both of type S and whose output is of type T". Note that if the output type is Bool then it denotes a predicate-symbol instead of a function-symbol.
(Q6) ∀x∈S ( f(f(f(x))) = f(f(x)) ) ∧ ∀x∈S ∃y∈S ( x = f(y) ) ⇒ ∀x∈S ( f(x) = x ), where f : S→S.
(Q7) ∀y∈T ( f(g(y)) = y ) ∧ ∀x∈S ∃y∈T ( g(y) = x ) ⇒ ∀x,y∈S ( f(x) = f(y) ⇒ x = y ), where f : S→T and g : T→S.
(Q8) ∀x,y,z∈B ( p(x) = p(y) ∧ p(y) = p(z) ⇒ x = y ∨ y = z ∨ z = x ) ⇒ ∀x∈B ∃y,z∈B ∀w∈B ( p(w) = x ⇒ w = y ∨ w = z ), where p : B→B.
PA (Peano Arithmetic):
(PA1) ∀k∈ℕ ∃m∈ℕ ( k = m·2 ∨ k = m·2+1 ), where "2" denotes "(1+1)".
(PA2) ∀k,m,n∈ℕ ( 4 | k·k ∨ 4 | k·k+3 ), where (infix) | : ℕ^2→Bool is defined via ∀x,y∈ℕ ( x | y ⇔ ∃t∈ℕ ( x·t = y ) ).
(PA3) ∀k∈ℕ ( k > 1 ⇒ ∃p∈ℕ ( p > 1 ∧ p | k ∧ ¬∃q∈ℕ ( 1 < q < p ∧ q | p ) ), where "1 < q < p" is short-hand for "1 < q ∧ q < p".
(PA4) ∀k,m∈ℕ ( k·k = m·m·2 ⇒ k = 0 ).
(PA5) ∀k,m∈ℕ ( m > 1 ∧ ¬∃d∈ℕ ( d > 1 ∧ d | k ∧ d | m ) ⇒ ∃x,y∈ℕ ( k·x = m·y+1 ) ).
For reference, these exercises are theorems to be formally proven using this Fitch-style natural deduction system for FOL.

« first day (1062 days earlier)      last day (1419 days later) »