Reading a paper entitled Predication in the Logic of Terms on p. 114 Fred Sommers made a simple argument as follows:
"June smiles at someone. Therefore, June smiles."
Sommers said that this argument cannot get proven in modern predicate logic, but shows how it can get proven in his system.
I don't recall how existential elimination works exactly, but do recall that the subtleties take a lot of carefulness to keep straight, so I'm not sure his claim correct.
Consider the following argument:
"Some cubic object contains something. Therefore, some cubic object is a container (or perhaps 'some cubic object contains.'"
I think that in term-functor logic (with a prefix scheme) that could proved as follows, letting C stand for a cube, I for a container, and S for something (the indexing matters here):
assumption 1. + C1 + I12 S2
by association, 1. 2. + + C1 I12 S2
by + simplification, 2. 3. + C1 I12
Can the above argument which concludes that some cubic object (or make it a nice and tidy cube, I suppose) is a container get proved in modern predicate calculus?