FOM: Quantifier question

[Torkel Franzen]

Harvey Friedman says:

  >It appears that the completeness of the axiomatization that you give
  >for "there are infinitely many x such that" without function symbols
  >would imply that this obeys the compactness theorem.
  > ...
  >Have I misunderstood what you were saying?

  Clearly the logic is not compact, and the completeness claim (for
languages without function symbols) concerned only single formulas:
"if a sentence A in this logic is valid, it is provable using the above
rules".