The axioms of L1+ZF aren’t intended to be exhaustive of the primitive concepts.
The first four axioms are an axiomatization of classical propositional logic. There are many axiomatizations that satisfy the truth tables of each of the six logical connectives (¬, →, &, ∨, ⊻, ↔︎). This one is specifically chosen because it is the one used on Metamath.
If one wants an axiomatization which treats negation (¬) and conjunction (&) as primitives, then the following does just that:
Ax. 1 'Noncontradiction 1': ⊢ ¬[A & ¬(A & A)]
Ax. 2 'Noncontradiction 2': ¬[(A & B) & ¬A]
Ax. 3: ¬[¬(A & ¬B) & [¬(B & C) & (C & A)]]
Ax. 4'Conjunctive modus ponens': ⊢¬(A & ¬B) , ⊢A ⇒ ⊢B
Definition of '→': (A → B) ≝ ¬(A & ¬B)
These axioms only establish the relation between possible states of affairs and their obtainment and non-obtainment. They don’t establish that any specific SoA (the atomic wff A) obtains or the existence of anything.
Axioms 5 through 11 and the auxiliary axioms 17 through 22 are intended for formalizing the concepts of quantity and identity, and they posit that at least one thing exists in the actual world, although it doesn’t specify what that thing is (abstract or concrete). These are the axioms of first-order predicate logic with identity/equality.
Axioms 12 through 16 are axioms of Zermelo-Fraenkel Set Theory (ZF). They are intended as a foundation for mathematics. They posit the properties of sethood and the infinitude of distinct quantities (the important ones are Extensionality, Regularity, and Infinity). Although some of them can be replaced by other set-theoretic axioms, they are chosen because they are used on Metamath and sometimes I would need to cite their theorems.
In all, the axioms don’t posit the existence of anything concrete in the actual world, only abstract objects.