[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*From*: fl <freder...@xxxxxxxxxxx>*Date*: Fri, 4 Apr 2014 08:32:31 -0700 (PDT)*References*: <504901ef-294c-40d6-9697-6974220d6507@googlegroups.com> <665F32FD-0805-467D-9ADC-B8ABFB52207C@gmail.com>

In TLA+, tuples and sequences are functions. However, unlike in conventional presentations of ZF set theory, functions are not defined as relations (sets of pairs) but are primitive values, axiomatized by

IsAFcn(f) == f = [x \in DOMAIN f |-> f[x]]See also Section 16.1.7 of "Specifying Systems".In particular, << >> = { } is not provable in TLA+, nor is its negation.

Unconventional indeed. But what is defined here is the predicate IsAFcn not

the concept of function nor the operator [ x \in A |-> B ].

But what can we conclude from that ? That the theory

behind TLA+ is not ZFC but a theory (unspecified) less powerful than ZFC, or

that the definition of a function is not the definition we are accustomed to ?

As a rule I'm embarassed when a theory is defined by its semantic and not by axioms.

I think it's less clear.

But I suppose it would be too demanding.

Thank you for this answer.

--

FL

**Follow-Ups**:**Re: [tlaplus] << >> = { }***From:*fl

**References**:**<< >> = { }***From:*fl

**Re: [tlaplus] << >> = { }***From:*Stephan Merz

- Prev by Date:
**Re: [tlaplus] << >> = { }** - Next by Date:
**Re: [tlaplus] << >> = { }** - Previous by thread:
**Re: [tlaplus] << >> = { }** - Next by thread:
**Re: [tlaplus] << >> = { }** - Index(es):