I’ve been trying to express an axiomatic geometry (1) using a typed functional language (OCaml so far).
My motivation comes from (2) and the claim “Programs correspond to logical proofs”.
In particular, I understand it as, should the program compile and type-check, then the proof is valid.
So far I am struggling to even express a simple proposition resulting from 2 axioms:
- A1: for two points a, b, the segment ab is congruent to the segment ba
- A2: if ab is congruent to pq, and also congruent to rs, then pq is congruent to rs
- P1: for two points a,b, ab is congruent to ab (reflexivity of congruence).
I particularly struggle with expressing dependencies in function arguments. For example A2 is a function that takes two congruences as input and outputs a new one, provided that the two input congruences share the first segment.
How would one go about it?
I am aware of previous work done with theorem provers (Coq,..) for this particular geometry. My understanding of this area is limited, and I am not sure that they only use the type theory assumed in (2) (in addition to hiding lots of things under the hood).
(1) W. Schwabhäuser, W. Szmielew, A. Tarski (1983). Metamathematische Methoden in derGeometrie