Search All of the Math Forum:
Views expressed in these public forums are not endorsed by
NCTM or The Math Forum.


fom
Posts:
1,968
Registered:
12/4/12


feeble compactness in syntactic formalisms  a topological analysis of TarskiGivant
Posted:
Dec 6, 2013 1:42 AM


On two other occasions, I tried to talk about the fact that a typical recursivelygenerated language for a classical bivalent logic could be structured as a minimal Hausdorff topology.
Such a topology is feebly compact.
A collection of expressions, organized to satisfy the description of a topology, cannot be compact since the language must also support the representations of inconsistent sets of expressions.
Feeble compactness is strong enough to ground the compactness theorem with regard to satisfiable collection. It is weak enough to admit the use of Koenig's lemma to identify finite sets of inconsistent formulas from an arbitrarily given inconsistent set.
Koenig's lemma is needed  or, possibly just the weak Koenig's lemma  so that such a finite set may be obtained using a systematic semantic tableaux as described by Smullyan.
====
In "A Formalization of Set Theory Without Variables" Tarski and Givant give five axioms describing the turnstile relation for an uninterpreted syntactic formalism.
What follows is some thoughts with respect to those axioms.
Tarski and Givant are careful to restrict the notion of a formalism to the kind of systems they are considering. But, their general description is rather simple:
"..., but also to formalisms *G* provided exclusively with syntactical components, and thus construed as ordered pairs,
< *G*,  >.
"Such formalisms are often referred to as syntactical or uninterpreted formalisms (as opposed to the original or interpreted formalisms). We can thus arrive at an abstract theory of syntactical formalisms, i.e., the theory of all ordered pairs
< *Sigma*,  >
(where  is a binary relation between subsets of *Sigma* and elements of *Sigma*."
I will be interpreting subsets of the system as global functions on the domain. Those with significant knowledge of the lambda calculus may see similarities of which I am unaware. I am considering these axioms in other contexts. In particular, I shall interpret these global functions as "selections".
Let X and Y be in *Sigma*. Let Phi, Psi, and Delta be subsets of *Sigma*.
Their first axiom is
"If ( X in Phi ), then ( Phi  X )"
Topologically, this describes a neighborhood filter about X. That is, one has
{ X }  X
{ X, A }  X
{ X, A, B }  X
{ X, A, B, C }  X
{ X, A, B, C, ... }  X
with respect to every pairing,
{ X }  X
{ X, B }  X
{ X, B, C }  X
{ X, B, C, ..., A, ... }  X
and so on.
For the purpose of expressing this interpretation of the axiom in the sense of a topological neighborhood, consider rewriting the axiom as,
"If ( {}_f in nbhd(X) ), then ( {}_f accepts X )"
There will be some complexity associated with this topological notion which is comarable to what is found in the set theory axioms. But, it is best to proceed to the additional axioms before discussing the issue.
Their second axiom is
"If ( Phi  Y ) for each ( Y in Psi ), and if ( Psi  X ), then ( Phi  X )"
This is clearly a transitive closure operation.
In terms of finitary wellformed formulas for which the reflexive relation of axiom 1 is excluded, this corresponds to a directed acyclic graph.
Now, consider this in the context of ZermeloFraenkel set theory for a moment. The axiom of foundation expresses the fact that the universe of sets is partitioned into those with the empty set as an element and those without that member. This is not a standard characterization of that axiom. But, when the empty set is an element of a set, the axiom is trivially satisfied.
This is easy to see with the initial example above. Consider the difference between the presentation,
{ X }  X
{ X, A }  X
{ X, A, B }  X
{ X, A, B, C }  X
{ X, A, B, C, ... }  X
and the presentation,
{ A }  X
{ A, B }  X
{ A, B, C }  X
{ A, B, C, ... }  X
With respect to interpreting X as the empty set, the turnstile relation may be interpreted as the converse of
"X is an element of the transitive closure of Y"
But, while the theory of pure sets has only the empty set as a set without members, a syntactic system has an antichain of incomparable syntactic atomic wellformed parts.
Suppose, now, that one tries to rewrite the second axiom as discussed earlier. Then one has something along the lines of
"If ( {}_f accepts Y ) and if ( {}_g in nbhd(Y) ) for each Y such that ( {}_f accepts Y ), then ( {}_g accepts X ) implies ( {}_f accepts X )"
For comparison, here is the original axiom:
"If ( Phi  Y ) for each ( Y in Psi ), and if ( Psi  X ), then ( Phi  X )"
To get a better sense of what is intended here, consider reading "accepts" as "selects". It is certainly true that this reading as a "selection" does not quite seem correct since the initial segment of a deduction could have several possible successor steps on the basis of transformation rules.
But, that is the point. The characterization given by Tarski and Givant is from subsets to individuals. At this level of abstraction, those dependencies are obscured and the specification is that of a fixing a single element from among alternatives. The sense of "selection" corresponds with unspecified modal alternatives. The sense of "acceptance" corresponds with a unique selection for any given instantiation.
The wikipedia link,
http://en.wikipedia.org/wiki/Transitive_closure#In_graph_theory
expresses the fact that the transitive closure operation on a directed acyclic graph yields a strict partial order. I have promoted the idea that a single formal expression could suffice in the construction of theories. That statement is schematized by this expression conveying an irreflexive transitive order,
AxAy( x irreflx y <> ( Az( y irreflx z > x irreflx z ) /\ Ez( x irreflx z /\ ~( y irreflx z ) ) ) )
The next section from the link above,
http://en.wikipedia.org/wiki/Transitive_closure#In_logic_and_computational_complexity
discusses the fact that this is a fixed point logic which is more expressive than the usual notions of a firstorder logic. If one follows the links to the page,
http://en.wikipedia.org/wiki/NL_%28complexity%29
one finds that this logic has a complexity class referred to as "nondeterministic logarithmic space". As it is expressed according to
NL=NSPACE(log n)
it is, unfortunately, not of any use to logic programmers,
http://en.wikipedia.org/wiki/Nondeterministic_space
On the other hand, it is closely related to certain ideas in the foundations of mathematics toward which I am inclined to have some minor interest. And, I am personally uninterested in foundational perspectives based upon metaphysically grounded distinctions.
This is a particular construction with a welldefined complexity and appropriate features for mathematical discourse of all variety.
The difficulty mentioned earlier begin to appear when we recognize that the first axiom yields expressions of the form,
{ X }  X
This has a great deal in common with Zermelo's original formulation of set theory. His original version relates singletons to denotations and uses the sign of equality to relate denotations. This notion had been changed as the formalisms recommended by Skolem had been implemented.
For the present purposes, one may formulate the expression
( {}_X=X accepts X )
Interpret this as one will. It can reflect the "arrow only" interpretation of category theory. It can reflect the ambiguous syntax of point set topology wherein '{x}' is identified with 'x' as a syntactic stipulation. It can be a graphtheoretic notion of selflooping. Pick a favorite belief. This exposition is not at the level of an object theory.
The sense by which induction is inherently impredicative arises with the transitive closure logic and its fixed point characteristics. The reflexive case is an augmentation to the strict partial order given by the transitive closure logic.
This can be made precise by considering a single "true" instance of the axiom above. Let '<' be used to express the asserted relation and let '>=' be used with its usual sense in relation to '<'. One can consider "accepted", "undecided", and "omitted" formulas based on an iteration.
For example,
accepted: { a < b, a < c } omitted: { b < c } undecided: { b >= c }
accepted: { a < b, a < c, a < d } omitted: { b < c, c < d } undecided: { b >= c, c >= d, b >= d }
accepted: { a < b, a < c, a < d, a < e } omitted: { b < c, c < d, d < e } undecided: { b >= c, c >= d, b >= d, d >= e , c >= e , b >= e }
and so on.
Several things can be observed here.
First, the the accepted formulas for each instance describe a pointed set of language parameters. Second, the accepted types are specifying a partial collection of ordered pairs satisfying the diversity relation ( ~x=y ) by means of a single ordered pair. Hence, one can partition the diversity relation in such a way that the two components of the partition separate into one with semantical content and one without, where the two components are also relational converses. Third, the undecided formulas comprise a bounded chain. However, subsequent axioms could omit or accept formulas according to any partial order that does not violate the omitted types.
Augmenting this irreflexive transitive order with a reflexive relation introduces a very significant problem.
Proper filters are characterized by the finite intersection property. Neighborhood filters only satisfy this property when they are principal filters with respect to a single individual. An antichain of ordertheoretic atoms would have empty intersection.
Boolean logic provides a means of addressing this problem for formal set theories. By analogy, the recursive construction of a formal language supports the same method.
In set theory, every set is associated with a singleton and the axiom of pairing can form finite sets. In the typical recursive construction of a countable language, every finite collection of wellformed formulas can form pairwise connected terms.
In both cases, the failure of the finite intersection property for the collection of neighborhood filters is compensated by the existence of an element that corresponds with the intension of finite intersection or finite conjunction. This element exists as an individual in the theory.
This is not, however, an ad hoc mechanism. In set theory, the axiom of pairing in conjunction with the axiom of union implements a directed set structure. This is implicit to theories of arithmetic by virtue of the difference relation.
It is inherently arithmetical, hence mathematical.
To make this work in set theory, however, one needs the axiom of pairing interpreted in the sense of matroid circuits.
Matroid theory is robust enough to distinguish matroids corresponding to graphical selfloops from matroids which correspond to a collection of singletons interpreted as parallel classes.
Yet, the definition of parallel classes in matroid theory for a set of singletons also presupposes that pairs form circuits for such a matroid.
For set theory, the consequence of this view is that the "mereological" nature of the proper subset relation has no large cardinal strength. This is explained by Hamkins in the link,
http://mathoverflow.net/questions/144231/istheinclusionversionofkuneninconsistencytheoremtrue
For the formal language, one requires something along the same lines. Although Boolean logic provides binary connectives, the machinery is not sufficiently weak to convey the sense of mereological weakness one finds in set theory.
The notion of pairing which is needed would be a single connective  a complete connective. Given any two formulas, there is a formula corresponding to its pair. That the pair is interpreted as a truthfunctional connective is secondary. However, the reason for associating pairing with a complete connective is so that pairing is semantically weak until semantically strengthened through interpretation.
As I have explained elsewhere, the system of basic Boolean functions can be represented in such a manner that a system could use a complete connective in just this manner. In my formulations, the NOR connective has the semantic significance. Consequently, one could formulate the language recursively using the NAND connective as a purely syntactic construct.
What I describe as mereological weakness for set theory is expressed by the understanding that the recursive formulation of the language is supported by the 4096 axioms in the link,
https://groups.google.com/forum/#!original/sci.logic/zuLUred6O3U/cH_nH7GCKjYJ
Unfortunately, when one "knows" what one means in a truth table, one fails to understand that the recursive construction of a language as a purely syntactic matter ought to be based upon axioms just as the transformation rules may be formulated axiomatically. Although this is a simple idea, it makes it difficult for using the syntax effectively. These constructions are intended to ground typical use, not supplant it.
In recursive construction, there is a unary operation for prefixing a primitive quantification symbol. Such prefixing should be compared with the sequence of nested singletons in set theory as far as such an analogy may allow. What is important in the present discussion is the role of pairing.
Before turning to the third axiom, there is one additional issue to be mentioned. The sense by which the finite intersection property is "implemented by proxy" introduces a problem similar to what one sees in algorithmically random reals. The system contains repetitive information. However, the sense of atomic wellformed parts is that they be able to take on truth valuations without dependency.
Without prejudice, I view this as cause for rejecting systems of logical atomism. It does not seem that this problem can be solved by syntactic stipulations. Perhaps I am wrong.
For their third axiom, Tarski and Givant have the following:
"If ( Phi  X ), then ( Delta  X ) for some finite ( Delta subset Phi )"
This clearly resembles a statement of compactness. Compare the form of the statement with
"Every open cover has a finite subcover"
That is an open set notion of compactness, and, it can be associated with consistent theories (in distinction from closed set models which may be associated with paraconsistent logics).
However, this is not quite the fact of the matter.
There are two cases. The first is where ( Phi  X ) is true for every X. In order to handle this case, one needs at least the weak Koenig's lemma. The discussion of compactness in Smullyan using Hintikka sets is what is required. A systematic tableaux applied to an inconsistent set will eventually yield a finite tree. However, it must be possible for the tree to contain an infinite branch in order to distinguish between a satisfiable collection and an unsatisfiable collection.
The second case relies on the fact that the insight of Frege had been to introduce "The True" and "The False" as objects.
The link,
http://books.google.com/books?id=DkEuGkOtSrUC&pg=PA119&lpg=PA119&dq=%22minimal+hausdorff+topology%22&source=bl&ots=3iJBPKz0j7&sig=ZPwm_43XRhgdJneeO82fUDZvZI&hl=en&sa=X&ei=YzOgUpPlN4azrgHqu4D4CQ&ved=0CEEQ6AEwAw#v=onepage&q=%22minimal%20hausdorff%20topology%22&f=false
has a diagram of an example of the minimal Hausdorff topology which makes this explanation simple.
The example begins with the Cartesian product of the positive integers Z^+ and the set,
{ 1, 2, 3, ..., w, ..., 3, 2, 1 }
To this set is added 2 arbitrary symbols. For the present purposes, we take these symbols to correspond with 'T' and 'F'.
In addition, we take the 'w' to correspond with the 'NAND' connective with which the formal language is recursively constructed.
Suppose one is given an enumeration of the wellformed formulas for a language. Then, for the first collection corresponding to the set above, take each formula P which contains no more than one atomic formula and form the pair,
NAND( P, P )
NAND( NAND( P, P ), NAND( P, P ) )
One can now use the enumeration to form the first set with the less complex formulas in the postive loci and the negated formulas in the negative loci.
For the next collection, choose only those formulas P which contain exactly two atomic formulas. Again form the pairs,
NAND( P, P )
NAND( NAND( P, P ), NAND( P, P ) )
and position them at their respective loci.
In this manner, one can use the complexity on atomic formulas to form the minimal Hausdorff topology for the language elements in the construction.
One now has an equisatisfiable subcollection of the originally generated formulas. Taking this as the collection *Sigma* provides a language with the appropriate topological structure for implementing the third axiom.
This is very similar to the kind of conditioning Kolmogorov implemented to formulate notions surrounding the law of excluded middle important to intuitionistic and constructive reasoning. In this case, however, it is being done to support the topological structure of a classical, compositional logic.
There are two properties which make this construction of a minimal Hausdorff space significant. Such spaces are Hausdorffclosed and semiregular.
Every Hausdorff space can be densely embedded into an Hclosed space, and, in the class of Hclosed spaces, there is a particularly important Hclosed extension called the Katetov extension. With respect to this extension, the original space is an open set. The Katetov extension is defined with respect to the free open ultrafilters, its extended elements comprise a discrete closed set, and the Katetov extensions of semiregular topologies can always be embedded into a minimal Hausdorff topology.
Since every Hausdorff space can be embedded as a nowhere dense subspace of a semiregular space, every Hausdorff space can be embedded into a minimal Hausdorff topology as a nowhere dense space. With respect to forcing models, every semiregular space can be densely embedded into a minimal Hausdorff topology.
Consequently, a minimal Hausdorff topology can embed densely into itself. This is characterized syntactically by the methods discussed above involving singletons, pairs, and finite intersections or finite meets.
To the extent that the third axiom expresses compactness, it is feeble compactness.
A space is feebly compact if every locally finite collection of open subsets of X is finite. For Hclosed sets, this translates into the properties,
1.
For every open cover of X, there is a finite subfamily whose union is dense in X
2.
Every open filter has nonvoid adherence
3.
Every open ultrafilter on X converges
Notice that the first statement is not compactness. The compactness theorem in logic is stated only with respect to satisfiable formulas whereas this construction involves the structure of uininterpreted syntax. But, consistent logics are associated with topological semantics given by open topologies. So, feeble compactness expresses the sense of compactness in terms of open sets. But, it cannot express the notion of a finite cover since a consistent theory cannot include every formula.
The second statement reflects the fact that a consistent theory cannot have an empty domain in standard firstorder semantics.
The third statement reflects the notion above concerning fixed point logics.
For minimal Hausdorff topologies, one has, in addition:
Every open filter with a unique adherent point converges.
I would presume this corresponds to being able to assume a first expression as being true. For typical constructions based upon "ontological" notions of identity, that might be the formula,
Ax( x=x )
for example.
It may also correspond with the weak weak Koenig's lemma in the sense that a finite tree is pruned with increasing length. Hence, there is a sense by which infinite length is approached by asymptotically fewer branches. In particular, the axiom above would have a tableaux consisting of one infinite branch.
However, the stronger notion is required to deal with the inconsistent case. One cannot know which branches of a systematic semantic tableaux can be pruned until they are closed. No asymptotic condition can be given in advance.
All of these topological relations may be found in "Extensions and Absolutes of Hausdorff Spaces" by Porter and Woods.
To the extent that these topological notions translate into consistent theories, I have elsewhere proven that a consistent firstorder theory is associated with a proximity on its langauge terms. Awodey has shown that necessary denotations are continuous denotations in topological semantics for first order logic. To the extent that one is speaking of the turnstile relation in the present context, necessary denotations may be considered to be in correspondence with eliminable definite descriptions.
In terms of the functional notation, the third axiom,
"If ( Phi  X ), then ( Delta  X ) for some finite ( Delta subset Phi )"
might be recast along the lines,
"If ( {}_f selects X ), then there exists {}_g such that ( {}_g selects X ) and ( {}_g in nbhd(Y) ) for only finitely many Y for which ( {}_f in nbhd(Y) ) holds"
Next, fourth and fith axioms given in Tarski and Givant should be considered together. These axioms are:
"*Sigma* is countable"
"There is a finite ( Delta subset *Sigma* ) such that ( Delta  Y ) for each ( Y in *Sigma* )"
Recast these axioms as
"Given any distinct {}_i and {}_j, one has that dom( {}_i ) = dom( {}_j ) and dom( {}_i ) is countable"
"For each Y there exists {}_i such that ( {}_i in nbhd(X) ) for finitely many X and such that ( {}_i accepts Y )"
Taken together, these axioms seem to assert the existence of an omegaregular filter. A filter F over a domain D is an omegaregular if and only if there exists a set E such that ( E subset F ), ( E = omega ), and for each ( d in D ) there exist only finitely many ( e in E ) such that ( d in e ).
Every omegaregular filter is countably incomplete.
Since every open filter has nonvoid adherence, this cannot be an open filter.
But, such a filter is necessary. Seemingly, this filter would correspond to the filter associated with fallacies. By the nature of omegafilters, to the best that I can discern, this filter would contain every finite set.
The existence of this filter has a number of consequences as discussed in Chapter 4 of Chang and Keisler. I have surveyed the various statements and found nothing obviously unsupportable with such a construction interpreted in this way.
This concludes a somewhat difficult analysis of the TarskiGivant axioms.



