Compactness Theorem for Some Generalized Second-Order Language
Bibliographic record
Abstract
For the first-order language the compactness theorem was proved by K. Gödel and A. I. Mal'cev in 1936. In 1955, it was proved by J. Łoś (1955) by means of the method of ultraproducts.Unfortunately, for the usual second-order language the compactness theorem does not hold.Moreover, the method of ultraproducts is also inapplicable to second-order models.A possible way out of this situation is to refuse the most vulnerable place in the construction of ultraproducts connected with the factorization relatively an ultrafilter, i.e., to stay working with the ordinary non factorized product.It compels us instead of the single usual set-theoretical equality = to use several generalized equalities ≈ first and ≈ second for first and second orders, and instead of the single usual set-theoretical belonging ∈ to use several generalized belongings < second .Following that it is necessary to refuse the usual set-theoretical interpretation (γ(x 0 ), . . ., γ(x k )) ∈ γ(u) of the second basic (after equality) atomic formula (x 0 , . . ., x k )u and to replace it by the generalized interpretation (γ(x 0 ), . . ., γ(x k ))<τ γ(u), where x τ i i are variables of the first-order types τ i , u τ is a variable of the second-order type τ = [τ 0 , . . ., τ k ] (i.e.predicate), and γ is some evaluation of variables on some mathematical system U.This paper is devoted to rigorous development of the expressed general idea.For the generalized in such a manner second-order language the compactness theorem is proved by means of the method of infraproducts consisting in rejection of the Łoś factorization.In the end of the paper the method of infraproducts is applied for the construction of some uncountable models of the second-order generalized Peano-Landau arithmetic.
Fetched live from OpenAlex and de-inverted. Abstracts are not stored in this database: the inverted indexes are 8.6 GB of the frame’s 9.3 GB of text, and the host has 13 GB free.
How this classification was reachedexpand
Full frame machine prediction
Teacher imitationNot calibrated prevalence, not ground truth. Human validation pending. The Gemma side is a direct model label for every work in the frame, read from the title-only record. The Codex side is a classifier learned from the 10,348 direct Codex labels and calibrated to design-weighted sample rates; fields without enough sample support carry no Codex call. Candidate is the union of the two sides; consensus is their intersection. These outputs are machine_predicted_unvalidated and are not human labels.
Distilled classifier scores by category (both heads)
| Category | Codex | Gemma |
|---|---|---|
| Metaresearch | 0.002 | 0.003 |
| Meta-epidemiology (narrow) | 0.000 | 0.000 |
| Meta-epidemiology (broad) | 0.001 | 0.002 |
| Bibliometrics | 0.001 | 0.001 |
| Science and technology studies | 0.002 | 0.004 |
| Scholarly communication | 0.002 | 0.007 |
| Open science | 0.001 | 0.003 |
| Research integrity | 0.001 | 0.002 |
| Insufficient payload (model declined to judge) | 0.005 | 0.001 |
Machine scores (provisional)
The two teacher heads of the student model, read on this work. A score orders the frame for review; it never asserts a category, and the validation status ships verbatim with every row.
Baseline scores from an immature model (maturity gate not passed, 7 training rounds). Scores rank; they never assert a category.
score_only:v0-immature-baseline · verbatim from the scoring run: score_only means the number may rank works, and no category label ships from itClassification
machine, unvalidatedMachine predicted; a candidate call from one source (direct Gemma or distilled Codex), not a consensus.
How this classification was reached, model by model and score by score, is at the end of the page under "How this classification was reached".