The notion of Formal Analyticity, with the specific acronym FAn (also used for the adjective Formal Analytic) is here introduced to make precise certain philosophical and other investigations here in Factasia.
The words are suggestive of a connection with the notion of analyticity, which however should not be taken as definitive. The definition of FAn is given below.
The following definition is given in terms of classical set theory. It is believed to be equivalent to definitions given in other terms, (e.g. topos theory, number theory, recursion theory) and it is only because of this equivalence that the concept is considered important.
It is intended that HOST will suffice to express all FAn statements in a reasonably direct way, and that other FAn languages will be interpretable by embedding into HOST.
A statement in formal language L is a FAn statement if L has a semantics rendered as an embedding into a classical set theory interpreted under the FAn semantics. A semantic embedding is a primitive recursive map from L into the language of set theory which is faithful to the meaning of the constructs in the language L.