If I understand correctly, you are saying that one can technically create an arbitrarily long axiom at any step, so the possibilities are infinite considering the action “add new axiom”.
I think Gurkenglas was saying something like “you could break down creating a new axiom in the steps it takes to write an axiom, like the actions ‘start axiom’, and then add a symbol/token (according to the available grammar).”
OpenAI was possibly mentioning that the number of actions is unbounded, like you could create an axiom, which becomes part of your grammar, and then have one more action, etc.
Where after “start axiom”, the next action would not be to add the leftmost character of the axiom’s string, but the topmost node of the abstract syntax tree, such as that it is a disjunction of 3 terms.
By the language’s grammar, it is infinite. You can introduce an infinity of axioms in any step of deduction.
If I understand correctly, you are saying that one can technically create an arbitrarily long axiom at any step, so the possibilities are infinite considering the action “add new axiom”.
I think Gurkenglas was saying something like “you could break down creating a new axiom in the steps it takes to write an axiom, like the actions ‘start axiom’, and then add a symbol/token (according to the available grammar).”
OpenAI was possibly mentioning that the number of actions is unbounded, like you could create an axiom, which becomes part of your grammar, and then have one more action, etc.
Where after “start axiom”, the next action would not be to add the leftmost character of the axiom’s string, but the topmost node of the abstract syntax tree, such as that it is a disjunction of 3 terms.