Mathematics - 2017-09-10 (page 2 of 6)

Secret

08:01

what programming language is this?

Kenny Lau

Prover9 is an automated theorem prover for First-order and equational logic developed by William McCune. Prover9 is the successor of the Otter theorem prover. Prover9 is intentionally paired with Mace4, which searches for finite models and counterexamples. Both can be run simultaneously from the same input, with Prover9 attempting to find a proof, while Mace4 attempts to find a (disproving) counter-example. Prover9, Mace4, and many other tools are built on an underlying library named LADR to simplify implementation. Resulting proofs can be double-checked by Ivy, a proof-checking tool that has been...

It managed to prove the existence of left inverse from the existence of right inverse + identity in 0.03 seconds

Assumptions:

all a exists b (a*b = 1).
all a all b all c a*(b*c) = (a*b)*c.
all a a*1 = a.

Goals:

all x exists y (y*x = 1).

Proof:

1 (all a exists b a * b = 1) # label(non_clause).  [assumption].
2 (all a all b all c a * (b * c) = (a * b) * c) # label(non_clause).  [assumption].
3 (all a a * 1 = a) # label(non_clause).  [assumption].
4 (all x exists y y * x = 1) # label(non_clause) # label(goal).  [goal].
5 x * f1(x) = 1.  [clausify(1)].
6 (x * y) * z = x * (y * z).  [clausify(2)].
7 x * 1 = x.  [clausify(3)].
8 x * c1 != 1.  [deny(4)].
10 x * (f1(x) * y) = 1 * y.  [para(5(a,1),6(a,1,1)),flip(a)].
11 x * (1 * y) = x * y.  [para(7(a,1),6(a,1,1)),flip(a)].

Secret

Hmm, I wonder what it will return when I put in the division by zero algebra axioms, hopefully it is robust enough to handle an arbitrary ringnoid

I already know the result for the finite case, but the infinite case is still open for associative algebras

(and I am too busy at chemistry to do further investigations in maths in general)

Kenny Lau

@Secret give me your axioms and your goals

I'll help you type them in

Secret

Axioms for infinite associative division by zero algebra:
1. $|S|$ is infinite
2. left additive identity 0+x=x for all x.
3. right zero inverse 0q=1
4. (I forgot whether left or right) multiplicative identity 1
5. Left distributive law a(b+c)=ab+ac
6. Associative law

(I might have mixed up some of the left right combinations, as the master documents is not with me currently)

Kenny Lau

I can't code 1

(and it's assumed implicitly anyway)

Secret

08:08

ok then put in 2-6 and see what the program said about it

Kenny Lau

@Secret oh, we're just checking if it's consistent?

Secret

Yes, if the No-Go Theorem is true for all associative algebras, I expect associative law will break

I already know the case for finite sets is relatively trivial with null semigroup stuff

If I do recall all axioms correctly, the program should not be able to simplify any products of zeros

and will just output them as it is

I will be back after the bath, let me know if the program found anything interesting

Kenny Lau

I still don't understand what your goal is...

 + :
       | 0 1 2
    ---+------
     0 | 0 1 2
     1 | 0 1 2
     2 | 0 1 2

 * :
       | 0 1 2
    ---+------
     0 | 2 0 1
     1 | 0 1 2
     2 | 1 2 0

 q : 2

The above is the "counter-example" generated for the assumptions below:

all x 0+x=x.
0*q=1 & q != 0 & q != 1.
all x x*1=x.
all x 1*x=x.
all a all b all c a*(b+c)=(a*b)+(a*c).
all a all b all c (a*b)*c=a*(b*c).
all a all b all c (a+b)+c=a+(b+c).

(it's actually an example for reasons I won't try to explain)

Secret

08:40

Back.
The above case is already known because all finite associative division by zero algebras must be composed of null semigroups, its extensions or a direct product of them (as it is evident in the + table that it is a right null semigroup)

What I am interested in is whether in the infinite case there exists examples that does not contain null semigroups

Leaky Nun

what is a null semigroup?

and can you check the set of axioms?

Secret

A null semigroup is a semigroup with an absorbing element. The element can be the unique two sided absorber, or can be either left or right absorbers

It's cayley table will be either a column of the same types of elements, or a row of them, or the whole table being the absorber, as shown in the wikipedia examples

Leaky Nun

so your goal is to prove that it must be a null semigroup?

Secret

What I proved last year is that all finite associative division by zero algebras must be a left or right null semigroup, or a concatenation of the cayley table of a finite number of right/left null semigroups. This is the No-Go Theorem that I always talked about

But I have yet to prove whether it also holds for infinite structures

The reasons for that is that in infinite dimensions, an injective map is not necessary surjective, thus it might provide an opening to allow "nontrivial" structures

Leaky Nun

 + :
       | 0 1 2 3
    ---+--------
     0 | 0 1 2 3
     1 | 0 1 2 3
     2 | 0 1 2 3
     3 | 3 3 3 3

 * :
       | 0 1 2 3
    ---+--------
     0 | 2 0 1 3
     1 | 0 1 2 3
     2 | 1 2 0 3
     3 | 3 3 3 3

 q : 2

Counter-example of the newly-added goal all x all y x+y=y.

Secret

08:48

No finite cases will be what I am looking for. What you generated here is the concatenation of the trivial semigroup {3} with the 3x3 right null semigroup (0,1,2)

It is still quite amazing that the program can re-generate these results so quickly while back then it took me at least 3 days to come up an example

Leaky Nun

I can't quantify over subsets in first order logic.

Secret

A corollary that I used to prove the no go theorem is that if the multiplication table contains a latin square, then its corresponding + table must be a null semigroup

Leaky Nun

@Secret would you just tell me what examples you want to see?

Secret

I want an example where you cannot find any columns/rows or subcolumns/subrows with the same element. For example, that L shape border of 3 is bad, the column of 1 and 2 is also bad, which according to the theorem, the set must be infinite.

Let me check the program to see whether it can do presentation-esch things to display infinite structures...

In order to do so, it means the * table cannot contain a latin square

(actually... I am not very sure if the latin square requirement is true for infinite sets, because when I do that proof, the fact that injective maps does no imply surjective for infinite sets allows an escape and thus I failed to prove that for the infinite case, thus it is still open)

Leaky Nun

@Secret for the addition or the multiplication?

Secret

08:55

Actually, I need BOTH tables to do that, which is why the structure must be infinite

Leaky Nun

look, I can't generate infinite examples.

Secret

I see, sorry...

Leaky Nun

 + :
       | 0 1 2 3 4
    ---+----------
     0 | 0 1 2 3 4
     1 | 0 1 2 3 4
     2 | 0 1 2 3 4
     3 | 4 4 4 3 4
     4 | 4 4 4 3 4

 * :
       | 0 1 2 3 4
    ---+----------
     0 | 2 0 1 3 4
     1 | 0 1 2 3 4
     2 | 1 2 0 3 4
     3 | 3 3 3 3 3
     4 | 4 4 4 3 4

I noticed the 3 column in the multiplication, wait

Secret

It's alright, if I have done my proof correctly, the program should not be able to generate any finite examples that can fullfill the requirement.

(I will be quite interested if it does, but then it must be a very large number cause the largest number of elements I have tested is 10 before I start writing the proof)

Leaky Nun

the program is not doing well

it will auto destruct in 1 minute

Secret

09:01

This particular 5x5 + table is quite interesting, though, I do not recall seeing something like 4 4 4 3 4 before...

Leaky Nun

time limit exceeded :D

removing one of my constraints gives you this:

 + :
       | 0 1 2 3 4
    ---+----------
     0 | 0 1 2 3 4
     1 | 0 1 2 3 4
     2 | 0 1 2 3 4
     3 | 4 4 4 3 4
     4 | 4 4 4 3 4

 * :
       | 0 1 2 3 4
    ---+----------
     0 | 2 0 1 3 4
     1 | 0 1 2 3 4
     2 | 1 2 0 3 4
     3 | 3 3 3 4 3
     4 | 4 4 4 3 4

 q : 2

Secret

hmm....

* 3 *
3 4 3
* 3 *
that seems new... I will check later and see if I have such examples...

Leaky Nun

 + :
       | 0 1 2 3 4 5 6
    ---+--------------
     0 | 0 1 2 3 4 5 6
     1 | 0 1 2 3 4 5 6
     2 | 0 1 2 3 4 5 6
     3 | 3 3 3 3 5 5 3
     4 | 4 4 4 6 4 4 6
     5 | 5 5 5 3 5 5 3
     6 | 6 6 6 6 4 4 6

 * :
       | 0 1 2 3 4 5 6
    ---+--------------
     0 | 2 0 1 3 4 5 6
     1 | 0 1 2 3 4 5 6
     2 | 1 2 0 3 4 5 6
     3 | 3 3 3 3 3 3 3
     4 | 4 4 4 4 4 4 4
     5 | 5 5 5 5 5 5 5
     6 | 6 6 6 6 6 6 6

 q : 2

ignoring multiplication gives you the above

this is so beautiful

Now my goals are:

  (all x all y x + y = y)
| (all x all y x * y = y)
| exists x (x != 0 & all y x + y = x)
| exists x (x != 0 & all y y + x = x)
| exists x (x != 0 & all y x * y = x)
| exists x (x != 0 & all y y * x = x).

I'm running the prover and the searcher at the same time

(the searcher searches for counter-examples)

@Secret do you have any specification?

both timed out.

Secret

The 7x7 table you generate fits nicely to the result of the theorem I proved (hence known), but the 5x5 table may be interesting, it does not seemed to fit the result of the theorem I proved. More investigation needed

Leaky Nun

2 mins ago, by Leaky Nun

@Secret do you have any specification?

Can you list the axioms again?

After this I'm going to explore on coding the finite ZF axioms :P

Secret

09:11

$\textbf{Axioms for finite associative division by zero algebra:}$
1. $|S|$ is finite
2. left additive identity 0+x=x for all x.
3. right zero inverse 0q=1
4. Left multiplicative identity 1
5. Left distributive law a(b+c)=ab+ac
6. Associative law
$\textbf{No-Go Theorem}$
Let $(S,+,*)$ be a division by zero algebra. If $|S| < \infty$ and associativity holds, then $(S,+,*)$ must contain at least one null semigroup like substructure in the + or * structure

@LeakyNun Don't worry, do the ZF stuff first, it's not urgent now

Leaky Nun

@Secret could you remember whether left or right?

come on...

Secret

@LeakyNun Let's say left

Leaky Nun

also, is the associative law for addition or multiplication?

Secret

Both (else it is not an associative algebra)

Leaky Nun

+ :
       | 0 1 2 3
    ---+--------
     0 | 0 1 2 3
     1 | 1 0 3 2
     2 | 1 0 3 2
     3 | 0 1 2 3

 * :
       | 0 1 2 3
    ---+--------
     0 | 3 2 1 0
     1 | 0 1 2 3
     2 | 3 2 1 0
     3 | 0 1 2 3

Searcher found.

This is most exciting.

Secret

09:14

I think I might be too strict to call
3 2 1 0
3 2 1 0
a null semigroup...

But sure

Leaky Nun

@Secret any additional rule?

Secret

27 mins ago, by Leaky Nun

I can't quantify over subsets in first order logic.

We cannot check for substructures, so I guess the only thing we can do is find some particular examples within by adding extra assumptions

Let me think...

try adding 1+3=2

After this one I think I will like to see your ZF stuff instead

Leaky Nun

@Secret look, just tell me what you want to do

it might not require quanitfying over subsets

Secret

Ok here's the recipe for this particular cases:
1. |S| is finite
2. left additive identity 0+x=x for all x.
3. right zero inverse 0q=1
4. Left multiplicative identity 1
5. Left distributive law a(b+c)=ab+ac
6. Associative law
7. 1+2=3

Leaky Nun

@Secret I haven't started yet

 + :
       | 0 1 2 3
    ---+--------
     0 | 0 1 2 3
     1 | 1 0 3 2
     2 | 1 0 3 2
     3 | 0 1 2 3

 * :
       | 0 1 2 3
    ---+--------
     0 | 3 2 1 0
     1 | 0 1 2 3
     2 | 3 2 1 0
     3 | 0 1 2 3

 q : 2

I can't directly code "1+2=3" for some reason, so I replaced it with "1+q != q"

(since q is automatically 2)

@Secret anything new?

Secret

09:26

No, it's all good for now

While I do have another algebraic structure that is not a zero term algebra I am interested in, I forgot its axioms and will check later

Leaky Nun

@Secret you expressed concern over the repeated rows

should I elimiante them?

should I make addition a latin square?

YOUSEFY

Hi I have a question regarding the sum of absolute value:

$2 \sum_{j=0}^{i} |2j-i|$ is it equal to $2 \sum_{j=0}^{i} 2j-i + 2 \sum_{j=0}^{i} -2j+i| $

Secret

@LeakyNun Do not allow latin squares, and eliminate the repeated rows. If my proof is correct, it should failed to give any examples except the trivial ring

YOUSEFY

Is this correct?!

Leaky Nun

@Secret do not allow?

Secret

09:31

It can be proved by homomorphism over + that any latin square in * will result in the + structure to be a null semigroup because given $0+x=x$, $\phi (0)+\phi (x) = \phi (x)$

thus latin squares turn multplication into a permutation map

Leaky Nun

so do not care if it is a latin square?

but you mentioned that 3 2 1 0 3 2 1 0 is bad

Secret

I mean, avoid anything that look like e.g.:
1 2 3
2 3 1
3 1 2
to appear in the tables

and remove repeated rows

Leaky Nun

time limit exceeded

there must be repeated rows.

Secret

Right, so that means my proof is ok

Leaky Nun

For some reason 0 and 1 are the only allowed numbers

if I need 2 I would have to make it q and specify that q != 0 & q != 1

Secret

09:39

I guess that's just how the program works and notate elements

Leaky Nun

usukidoll

^ what class is that?

Leaky Nun

@usukidoll class?

usukidoll

ya or what book did that info came from?

Leaky Nun

I just searched online

privetDruzia

09:46

Hi

Could someone tell me what SO and SE mean in this text?

*SO(3) and SE(3)

Leaky Nun

@privetDruzia Special Orthogonal Matrix, Special Euclidean Group

privetDruzia

@LeakyNun Thanks!

Leaky Nun

Assumptions:

all x all y all z ((x*y)*z = x*(y*z)). %G1
all x (x*e=x & x=e*x). %G2
all x exists y (x*y=e & e=y*x). %G3

Goals:

all x all y x*y=y*x.

The following table for the smallest non-abelian group is generated in 0 seconds:

   | 0 1 2 3 4 5
---+------------
 0 | 0 1 2 3 4 5
 1 | 1 0 3 2 5 4
 2 | 2 4 0 5 1 3
 3 | 3 5 1 4 0 2
 4 | 4 2 5 0 3 1
 5 | 5 3 4 1 2 0

This is very exciting.

(cc @Secret)

Secret

10:03

Something 6, let me check...

Leaky Nun

@Secret this isn't related to the zero-division thing

Secret

I know, but I forgot the smallest non abelian group's name

Leaky Nun

10:16

Assumptions:

all x all y all z ((x*y)*z = x*(y*z)). %G1
all x x*e=x. %G2
all x x*inv(x)=e. %G3

Goal:

all x inv(inv(x))=x.

Proof:

1 (all x all y all z (x * y) * z = x * (y * z)) # label(non_clause).  [assumption].
2 (all x x * e = x) # label(non_clause).  [assumption].
3 (all x x * inv(x) = e) # label(non_clause).  [assumption].
4 (all x inv(inv(x)) = x) # label(non_clause) # label(goal).  [goal].
5 (x * y) * z = x * (y * z).  [clausify(1)].
6 x * e = x.  [clausify(2)].
7 x * inv(x) = e.  [clausify(3)].
8 inv(inv(c1)) != c1.  [deny(4)].
9 x * (e * y) = x * y.  [para(6(a,1),5(a,1,1)),flip(a)].
10 x * (inv(x) * y) = e * y.  [para(7(a,1),5(a,1,1)),flip(a)].

@Secret

Secret

Right $D_6$ dihedral group of 6 elements

Leaky Nun

@Secret right, it's also $S_3$ the symmetric group of 3 letters

@AlessandroCodenotti buongiorno

@Secret is the proof legible to you?

Expanded proof:

1 (all x all y all z (x * y) * z = x * (y * z)) # label(non_clause).  [assumption].
2 (all x x * e = x) # label(non_clause).  [assumption].
3 (all x x * inv(x) = e) # label(non_clause).  [assumption].
4 (all x inv(inv(x)) = x) # label(non_clause) # label(goal).  [goal].
5 (x * y) * z = x * (y * z).  [clausify(1)].
6 x * e = x.  [clausify(2)].
7 x * inv(x) = e.  [clausify(3)].
8 inv(inv(c1)) != c1.  [deny(4)].
9A x * y = x * (e * y).  [para(6(a,1),5(a,1,1))].
9 x * (e * y) = x * y.  [copy(9A),flip(a)].

hi @Fawad

Fawad

@LeakyNun hi!

Leaky Nun

> para(47(a,1),28(a,1,2,2,1)) -- paramodulate from the clause 47 into clause 28 at the positions shown.

Secret

@LeakyNun stuff in square brackets and the symbol c1 is not very understood by me, but the proof itself otherwise is legible

Leaky Nun

10:30

@Secret the stuff in square brackets is the steps used

paramodulate is basically "substitute"

% number = 1
% seconds = 0

% Interpretation of size 6

 * :
       | 0 1 2 3 4 5
    ---+------------
     0 | 0 1 2 3 4 5
     1 | 1 0 3 2 5 4
     2 | 2 4 0 5 1 3
     3 | 3 5 1 4 0 2
     4 | 4 2 5 0 3 1
     5 | 5 3 4 1 2 0

 e : 0

 c1 : 1

 c2 : 2

 inv :
         0 1 2 3 4 5
    ----------------
         0 1 2 4 3 5

it actually gives you a table for the inverse

oh, and of course c1 and c2 are where the goal fails: 1*2=3!=4=2*1

counter-example 1, I suppose

@Secret prover9 proves everything by contradiction

Leaky Nun

@Secret you might be more interested in the following puzzle:

of course prover9 has a built-in equal, but I decided to build my own

Assumptions:
all x equal(x,x).
all x all y (equal(x,y) -> equal(y,x)).
all x all y all z (equal(x,y) & equal(y,z) -> equal(x,z)).
all x equal(add(x,0),x).
all x all y equal(add(x,S(y)),S(add(x,y))).
Goals:
equal(add(S(0),S(0)),S(S(0))).

Can you construct a counter-example?

Also, why does it fail?

@Danu can I ask you a favour?

Little Rookie

4

Q: Question regarding Gambler's Ruin

Consider a gambling process $(X_n)_{n∈\mathbb{N}}$ on the state space $S = {0, 1, . . . , N}$, with probability $p$, resp. $q$, of moving up, resp. down, at each time step. For $x = 0, 1, . . . , N$, let $τ_x$ denote the first hitting time, $τ_x := \inf\{n ≥ 0 : X_n = x\}$ Let $p_x := P(τ_{x+1} <...

Secret

Let me translate:
\begin{align}
x & \sim x\\
x \sim y & \implies y \sim x\\
x \sim y & \text{ and } y \sim z \implies x \sim z\\
x + 0 & \sim x\\
x+S(y) & \sim S(x+y)
\end{align}
=> S(0)+S(0)=S(S(0))

Leaky Nun

10:45

you forgot the symmetric

btw, some theory: our input is in the form of "given A prove B". What prover9 does is to prove that A and not B leads to contradiction. Why it does this is because A and B can be consistent, at the same time with A and not B being consistent.

Dattier

Hi, is there non-dogmatic reasoning (not based on rules, principles, axioms or doctrines) ?

Leaky Nun

@Dattier bonjour, as-tu lu ma reponse sur ta question?

Dattier

Non, je ne l'ai pas vu

Leaky Nun

19 hours ago, by Leaky Nun

@Dattier $\begin{array}{cl} &\gcd(2^m+1,2^n+1) \\=& \gcd(2^m+1-2^{n-m}(2^n+1),2^n+1) \\=& \gcd(2^{n-m}+1,2^n+1) \end{array}$

19 hours ago, by Leaky Nun

and $\gcd(2^a+1,2^0+1)=2$ when $a$ is odd

la preuve de ton theoreme

Topologicalife

Hi.

Why $\left|\dfrac{xyz}{x^2+y^2+z^2}\right| \leq \left|\dfrac{x}{x^2+y^2+z^2}\right| \leq |x| \leq \left|\sqrt{x^2+y^2+z^2}\right |$ is not true?

For all $x,y,z \in \mathbb{R}$

Dattier

10:55

$$\begin{array}{cl} &\gcd(2^m+1,2^n+1) \\=& \gcd(2^m+1-2^{n-m}(2^n+1),2^n+1) \\=& \gcd(2^{n-m}+1,2^n+1) \end{array} \text{ and }\\ \gcd(2^a+1,2^0+1)=2$ when $a$ is odd$$

Leaky Nun

the first inequality fails when $|yz|>1$ @Topologicalife

Topologicalife

Right, uhm

Dattier

@LeakyNun : why you need a odd ?

Leaky Nun

sorry, $\gcd(2^a+1,2^0+1)=1$.

no matter $a$ is odd or even.

Topologicalife

$x \leq \sqrt{x^2+y^2}$ and $y \leq \sqrt{x^2+y^2}$ so is true that $xy \leq x^2+y^2$?

Dattier

11:00

But the result is not true when a, and b is even, for exemple a=4, b=2

@LeakyNun

Leaky Nun

$\gcd(2^4+1,2^2+1) = \gcd(17,5) = 1$

interesting

Dattier

and 2^2+1=5

gcd(2,4)=2

Leaky Nun

$\gcd(2^m+1,2^n+1) = \gcd(2^m+1-2^{m-n}(2^n+1),2^n+1) = \gcd(-2^{m-n}+1,2^n+1)$

my proof above was wrong

method abandoned :P

Secret

11:20

S(0) + 0 = S(0) = S(0+0)

still looking...

MEanwhile S(1)+S(1)=SS(1) is wrong since 2+2=3 (assuming you are doing the usual peano arithmetic)

Actually, give only these 5 assumptions, how does one derive S(S(0))?

Leaky Nun

you don't, you just keep it as-is.

Secret

S(0)+0=S(0+0)=S(0)
SS(0)+0 = S(S(0)+0) =SS(0)
S(0)+S(0) = S(0 + S(0))=SS(0)

nope, still consistent

I suspect S(0)+S(0) then not SS(0) is inconsistent, hence the whole system is consistent

since the above workings showed that S(0)+S(0)=SS(0)

Leaky Nun

S(0)+S(0) is not a statement...

"S(0)+S(0) then not SS(0)" is meaningless

@Secret then you need to check the above workings very carefully

Secret

S(0) + 0 = S(0)
0 + S(0) = S(0+0)=S(0)
what prevents x to be an element S(0) hence writing S(0) + S(0) = S(S(0)+0)=SS(0)?

Leaky Nun

The problem is in your second line

Secret

11:32

Let x = 0, y = 0, then x + S(y) = 0 + S(0). Then use x+ S(y) = S(x+y), this gives 0 + S(0) = S(0+0) = S(0)?

Leaky Nun

@Secret there is one unjustified step here.

Danu

@privetDruzia SO(3) is the group of rotations of $\Bbb R^3$:

Rotation group SO(3)

In mechanics and geometry, the 3D rotation group, often denoted SO(3), is the group of all rotations about the origin of three-dimensional Euclidean space R3 under the operation of composition. By definition, a rotation about the origin is a transformation that preserves the origin, Euclidean distance (so it is an isometry), and orientation (i.e. handedness of space). Every non-trivial rotation is determined by its axis of rotation (a line through the origin) and its angle of rotation. Composing two rotations results in another rotation; every rotation has a unique inverse rotation; and the identity...

SE is not really standard notation...

Secret

can we say 0 + 0 = 0 using x + 0 = x and set x=0?

Leaky Nun

@Secret yes you can

Secret

can we say x,y=0,0 and thus substitute x +S(y) to become 0 + S(0)?

Leaky Nun

11:34

@Secret yes, you can

Secret

can we then use x + S(y) = S(x+y), with x,y=0,0 to get 0 + S(0) to S(0+0)?

Leaky Nun

@Secret yes, you can

Secret

Then using:

2 mins ago, by Secret

can we say 0 + 0 = 0 using x + 0 = x and set x=0?

$S(0+0)=S(0)$, unless you mean S(0+0) and S(0) are different elements and not a map S acting on 0 and 0+0?

Leaky Nun

@Secret you can't actually prove that S(0+0)=S(0).

from 0+0=0.

Secret

that I don't understand, in terms of arguments, it makes sense, so that means S is not really a map, but something else altogether

Leaky Nun

11:38

@Secret maybe you never thought about why we can say $f(x)=f(y)$ when we know that $x=y$.

It's a property of equality that I didn't codify into my axioms.

It's actually an axiom schema.

Secret

Very likely, I just define maps directly in my algebraic structure, thus might be why I never noticed that

Leaky Nun

x=y iff P(x) iff P(y) for any proposition P

this is an axiom schema, one axiom per proposition

Secret

12:02

[Random]

x=y iff P(x) iif P(y) for all P

x=z iff P(x=y iff P(x) iff for all P) iff P(z)

x=a iff P(x=y iff P(x=y iff P(x=y iff P(x) iif P(y) for all P) iif P(x=y iff P(x) iif P(y) for all P) for all P) iif P(x=y iff P(x=y iff P(x) iif P(y) for all P) iif P(x=y iff P(x) iif P(y) for all P) for all P) for all P)

Dattier

12:17

the small theorem of Goldbach :
Let n be a natural, non-zero integer, there exists a finite sequence of natural distinct integers, prime or equal to 1, the sum of which is n.

Leaky Nun

12:33

@Dattier wow, never heard of it :)

Dattier

this is one of my enigmas

if the result existed before, I did not know it

@LeakyNun

Dodsy

12:50

what's a union of disjoint intervals?

Leaky Nun

a set?

Dodsy

@LeakyNun

imgur.com/a/bb9Kb

Leaky Nun

it means you express the solution as something like [0,1] union (2,3]

Dodsy

hm.

oddly the hand out he gave was very very basic

and the excersizes he gave were very very hard.

Transcript for

$Mathematics$ Mathematics