List Operations and Lambda Calculus
Passes 2-1
I don’t know if “Pairs and lists” is True or False, though…
/ Skju
Adminned at 23 Jun 2013 06:51:31 UTC
(If “Pairs and lists” is False, then so are the following):
Axioms:
* for all lists a, !a = b, where b is the head of a
* for all lists a, @a = c, such that a = (!a):c is true
* &x. is a function, with x as a single variable function, defined by the operation succeeding the “.” (e.g. &x.x is the identity function)
* for all lists a, where !a is a function, f(p), then #a = f(@a)
* IF is a function f(z) = #(z x y).
* T is a function f(x,y) = x
* F is a function f(x,y) = y
formalizing some operators and introducing some functional programming through lambda calculus, along with a conditional operator.
I’m just worried this is too much ‘programming’ oriented rather than pure math and proofs.
I don’t think that Tavros’ objections are too worrisome. Is the parenthetical condition at the top even valid? How can the title of a Proposal be true or false?
Tavros:
The first axiom says that !a is the head of a even if a is empty. This isn’t really problematic; the head of the empty list is undefined, so !{} will also just be undefined,
The second axiom entails that every list a can be written as !a : @a, even if a is empty. This also isn’t really problematic, but it is possible to prove, from the “Pairs and lists” axioms, that if {} = b:c, then c is not a list,
The third axiom is not a statement in first-order logic, since it appears to be defining infinitely many notations, but it would make a perfectly fine Rule,