This thesis is on the topic of set theory and in particular large cardinal axioms, singular cardinal patterns, and model theoretic principles in models of set theory without the axiom of choice (ZF). A standardised setup for the technique of our main tool, symmetric forcing, is established, in order to describe models that satisfy the approximation lemma. Sets of ordinals in such models are included in some model of set theory with the axiom of choice (ZFC). This enables the partial usage of previous knowledge about models of ZFC in the proofs. Most of the models are constructed using large cardinal strength and have cardinals with large cardinal properties. With the construction of such models it is shown that if we drop the axiom of choice from our requirements and assume a certain amount of large cardinal strength, several patterns of singular cardinals are possible and model theoretic properties such as higher Chang conjectures become much weaker in consistency strength. This thesis is written in a didactic style, in the hope that it will be useful for other researchers who want to use symmetric forcing with large cardinals for consistency strength studies.