Toki Pona Was NOT Meant For Math - Blog Posts

im sorry

remind me to rewrite this in the latin alphabet (sitelen Lasina) tomorrow

edit:

lon pi nanpa kipisi la [ante K ala la ante P ala] la [ante P la ante K]

( discrete math theorem: (~K => ~P) => (P => K) )

nasin lon

proof

(wan) [ante K ala la ante P ala] la [[ante K ala la ante P] la ante K]

(1) ((~K) => (~P)) => (((~K) => P) => K)

(tu) [ante K ala la ante P] la [[ante K ala la ante P ala] la ante K]

(2) ((~K) => P) => (((~K) => (~P)) => K)

(tu wan) ante P la [ante K ala la ante P]

(3) P => ((~K) => P)

(tu tu) ante P la [[ante K ala la ante P ala] la ante K]

(4) P => (((~K) => (~P)) => K)

(luka) [ante K ala la ante P ala] la [ante P la ante K]

(5) ((~K) => (~P)) => (P => K)

tan seme

why

(wan) lawa tu wan

(1) Axiom 3*

(tu) lon pi nanpa kipisi: ante P la [ante K la ante L]. ni la ante K la [ante P la ante L]

(2) discrete math theorem: ( P => (K => L) ) => ( K => (P => L))

(tu wan) lawa wan

(3) Axiom 1

(tu tu) lon pi nanpa kipisi: ante P la ante K. ante K la ante L. ni la ante P la ante L.

(4) discrete math theorem: P => K, K => L ⊢ P => L

(luka) lon pi nanpa kipisi: ante P la [ante K la ante L]. ni la ante K la [ante P la ante L]

(5) discrete math theorem: ( P => (K => L) ) => ( K => (P => L))

*so i went on Wikipedia to see if axiom numbers used in my class match up with what people usually use, and i found out that thing i was proving (i.e. contrapositive) is axiom 3 according to Wikipedia. however, in my class, axiom 3 is

"((~p)=>(~q)) => (((~p)=>q)=>p)"

so uh... yeah for the purposes of this post, ^ is axiom 3