Minimalistic type theory?

Stream: new members

[Mr Proof]

I was just playing about with type theory and seeing how many operators could I remove and it still be parseable.

e.g.

( P a a a ) Id
( P a P b a b a ) ImpIntro
( P a P b P c (a b) (b c) a c ) SelfImpType
( P a P b P c (a b) f (b c) g a x  g (f x) ) SelfImpProof
( N P f f 0 (N n f n f (S n)) (N n f n) ) Induct

To parse it use the rules:
P is a Proposition type.
[type] [type] = [type]->[type]
[type] [vari] = ForAll([vari]:[type]) or ([vari]:[type])=> (depending on context)
[func f] [term t] = f(t)

OK. Not very useful but interesting to see how stripped down you can make it. Till it just becomes lists of lists of symbols.

I also quite like this notation which is a little clearer:

( P.a P.b (a b).f a.x b.(f x) ).FuncApplyProof
( N.x S x ).addOne
( (N P).f f 0 (N.n f n f (S n)) (N.n f n) ).Induct

(this first is the proof of (a->b)->a->b) )

[Aaron Liu]

this is unreadable

[Mr Proof]

Yep. It's not for human consumption! :laughing:

[Aaron Liu]

is everything one letter?

[Mr Proof]

Doesn't have to be