Blog

[hacker-DOM]

I'm going back to finishing off amos-back tomorrow, thought I’d share a debrief:

• I created branches master (for releases, currently empty), develop and projectSetup. I just squash merged projectSetup into develop.
• The project setup (done) required somebody at mediocre level in logic / foundations of mathematics, and pretty good level in js/babel. I think this will reverse going forward (somebody >= mediocre in 'babelscript' and good in logic.
• I have dirs /propositions, /predicates and /sets for propositional, predicate and set theory, respectively
• my goal was to prove there exists an empty set (in the notation in the code, it’s S._existsUnique (x) (S._isEmpty (x)).
  I started with a warm-up theorem: A implies A (in the notation in the code: x => x >> x. I was able to prove this using only Hilberts first two axioms and Modus Ponens. It’s not difficult.

I first started with a _State constructor that included (axioms) and (inferences). I decided to hard-code MP (Modus Ponens) into _State, and that was a mistake - I was not able to use a basic inference rule (from A, B, deduce A and B).

The project needs more work in Propositional logic. We need to generalize the notion of MP and create an inferences state variable. Inferences should be provable just like predicates right now. I guess proving (from A,B, deduce A and B) would be a good start.

I'm using CVUT: Mathematical Logic and Oxford Maths institute Set theory as the blueprint. If somebody wants to contribute, it might be easier if we work from one text. Both are available for printing or download to tablet or desktop.

Btw Everything is MIT-licensed, which reads as "anyone can clone / fork this project and distribute it for free / for money, but they have to mention that they are using software creating by SF" (see Notice Condition here

If you have any q's, please reach out !

[hacker-DOM]

Ok I'll just use this thread for any comments.

I'm currently working on a branch called setup-2.

The goal is to get Babel, Typescript, Eslint and Mocha to work together, which is proving harder than expected. :D

Another goal is to completely transition to Typescript (0 errors).

My goal for this milestone is to prove there exists a unique empty set.

Also I'm getting rid of _State, all proof will be direct (in a sense FP as opposed to OOP).

A technical question that I don't know the answer to yet is whether to use functions for propositions, or objects. Previously I used functions for axioms, but once the axiom was used it became an object (a _Nand of some structure). I'm trying out refactoring everything to functions...

[hacker-DOM]

Ok just went deep in the first three technologies listed above.

We want to use

• Typescript, because it makes it easier to scale and read code,
• Babel, bc it has cool features like piping, but most importantly it allows plugins (Typescript didn't support compiler plugins.)

Given our setup, we want to run babel first, then check the types.

@babel/plugin-syntax-typescript and @babel/plugin-transform-typescript are perfect for that.

Now things get hard only when we need linting

• use VSCode Language Features (I think this uses TSLint under the hood, but not sure)
• use TSLint (wouldn't work on overloaded operators)
• use typescript-eslint - uses typescript compiler for linting [1]
• babel-eslint - uses babel for linting. The only problem is, even being on version @11.0.0-beta, it doesn't work that well with typescript. [1] [2]

Since Babel is more important for this project than Typescript, I'm going with babel-eslint. So I'm going to disable some linting rules (no-unused-vars, no-useless-constructor...) and hope that it will soon be fixed. 🙏